Metamath Proof Explorer


Theorem dvhfvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses dvhfvadd.h
|- H = ( LHyp ` K )
dvhfvadd.t
|- T = ( ( LTrn ` K ) ` W )
dvhfvadd.e
|- E = ( ( TEndo ` K ) ` W )
dvhfvadd.u
|- U = ( ( DVecH ` K ) ` W )
dvhfvadd.f
|- D = ( Scalar ` U )
dvhfvadd.p
|- .+^ = ( +g ` D )
dvhfvadd.a
|- .+b = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )
dvhfvadd.s
|- .+ = ( +g ` U )
Assertion dvhfvadd
|- ( ( K e. HL /\ W e. H ) -> .+ = .+b )

Proof

Step Hyp Ref Expression
1 dvhfvadd.h
 |-  H = ( LHyp ` K )
2 dvhfvadd.t
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhfvadd.e
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhfvadd.u
 |-  U = ( ( DVecH ` K ) ` W )
5 dvhfvadd.f
 |-  D = ( Scalar ` U )
6 dvhfvadd.p
 |-  .+^ = ( +g ` D )
7 dvhfvadd.a
 |-  .+b = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )
8 dvhfvadd.s
 |-  .+ = ( +g ` U )
9 eqid
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
10 1 2 3 9 4 dvhset
 |-  ( ( K e. HL /\ W e. H ) -> U = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )
11 10 fveq2d
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` U ) = ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) )
12 1 9 4 5 dvhsca
 |-  ( ( K e. HL /\ W e. H ) -> D = ( ( EDRing ` K ) ` W ) )
13 12 fveq2d
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` D ) = ( +g ` ( ( EDRing ` K ) ` W ) ) )
14 6 13 syl5eq
 |-  ( ( K e. HL /\ W e. H ) -> .+^ = ( +g ` ( ( EDRing ` K ) ` W ) ) )
15 14 oveqd
 |-  ( ( K e. HL /\ W e. H ) -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) )
16 15 3ad2ant1
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) )
17 xp2nd
 |-  ( f e. ( T X. E ) -> ( 2nd ` f ) e. E )
18 xp2nd
 |-  ( g e. ( T X. E ) -> ( 2nd ` g ) e. E )
19 17 18 anim12i
 |-  ( ( f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) e. E /\ ( 2nd ` g ) e. E ) )
20 eqid
 |-  ( +g ` ( ( EDRing ` K ) ` W ) ) = ( +g ` ( ( EDRing ` K ) ` W ) )
21 1 2 3 9 20 erngplus
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` f ) e. E /\ ( 2nd ` g ) e. E ) ) -> ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) )
22 19 21 sylan2
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( T X. E ) /\ g e. ( T X. E ) ) ) -> ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) )
23 22 3impb
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) )
24 16 23 eqtrd
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) )
25 24 opeq2d
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. = <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. )
26 25 mpoeq3dva
 |-  ( ( K e. HL /\ W e. H ) -> ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) )
27 2 fvexi
 |-  T e. _V
28 3 fvexi
 |-  E e. _V
29 27 28 xpex
 |-  ( T X. E ) e. _V
30 29 29 mpoex
 |-  ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) e. _V
31 eqid
 |-  ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } )
32 31 lmodplusg
 |-  ( ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) e. _V -> ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) = ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) )
33 30 32 ax-mp
 |-  ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) = ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )
34 26 33 eqtr2di
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) )
35 11 34 eqtrd
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` U ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) )
36 35 8 7 3eqtr4g
 |-  ( ( K e. HL /\ W e. H ) -> .+ = .+b )