Re: [mizar] the carrier of and [#]

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Wed, 4 Apr 2007, Jesse Alama wrote:
>
>> I faced a surprising problem recently concerning a seeming lack of
>> equality of
>>
>>  [#]V
>>
>> and
>>
>>  the carrier of V,
>>
>> where V has type VectSp of F, and F has type Field.  Specifically, the
>> statement
>>
>>  consider G being FinSequence of [#]V such that
>>    G is one-to-one and
>>    rng G = Carrier l and
>>    x - y = Sum (l (#) G) by VECTSP_6:def 9;
>> ::>                  *103
>>
>> where l is type Linear_Combination of A, A has type Subset of V, and x
>> and y have type Element of V, is rejected.  For reference,
>> VECTSP_6:def 9 is
>>
>>  definition let GF be non empty LoopStr;
>>             let V be non empty VectSpStr over GF;
>>             let L be Linear_Combination of V;
>>   assume A1: V is Abelian add-associative right_zeroed right_complementable;
>>   func Sum(L) -> Element of V means
>>    :Def9: ex F being FinSequence of the carrier of V st
>>      F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
>>
>> However, by changing "[#]V" to "the carrier of V", my statement is
>> accepted.  This surprised me, since, according to STRUCT_0:def 3, we
>> have [#]V = the carrier of V, and my original statement is rejected
>> even if I cite STRUCT_0:def 3.  What might be going on?
>
> Is STRUCT_0 listed in the 'definitions' directive? - only then the
> equals' definition works automatically - adding a subsequent reference
> to a universal sentence (the definitional theorem of STRUCT_0:def 3)
> won't help since the checker is able to use only one such universal
> premise in one disjunct in an inference.

Yes, STRUCT_0 is in my definitions directive.  Any other ideas for
what might be going on?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*950: Too many schemes (http://www.mizar.org)