Metamath Proof Explorer

Theorem dvhopvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dvhvadd.h 
|- H = ( LHyp ` K )
dvhvadd.t 
|- T = ( ( LTrn ` K ) ` W )
dvhvadd.e 
|- E = ( ( TEndo ` K ) ` W )
dvhvadd.u 
|- U = ( ( DVecH ` K ) ` W )
dvhvadd.f 
|- D = ( Scalar ` U )
dvhvadd.s 
|- .+ = ( +g ` U )
dvhvadd.p 
|- .+^ = ( +g ` D )
Assertion dvhopvadd 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+ <. G , R >. ) = <. ( F o. G ) , ( Q .+^ R ) >. )

Proof

Step Hyp Ref Expression
1 dvhvadd.h 
 |-  H = ( LHyp ` K )
2 dvhvadd.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhvadd.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhvadd.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dvhvadd.f 
 |-  D = ( Scalar ` U )
6 dvhvadd.s 
 |-  .+ = ( +g ` U )
7 dvhvadd.p 
 |-  .+^ = ( +g ` D )
8 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( K e. HL /\ W e. H ) )
9 opelxpi 
 |-  ( ( F e. T /\ Q e. E ) -> <. F , Q >. e. ( T X. E ) )
10 9 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> <. F , Q >. e. ( T X. E ) )
11 opelxpi 
 |-  ( ( G e. T /\ R e. E ) -> <. G , R >. e. ( T X. E ) )
12 11 3ad2ant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> <. G , R >. e. ( T X. E ) )
13 1 2 3 4 5 6 7 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( <. F , Q >. e. ( T X. E ) /\ <. G , R >. e. ( T X. E ) ) ) -> ( <. F , Q >. .+ <. G , R >. ) = <. ( ( 1st ` <. F , Q >. ) o. ( 1st ` <. G , R >. ) ) , ( ( 2nd ` <. F , Q >. ) .+^ ( 2nd ` <. G , R >. ) ) >. )
14 8 10 12 13 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+ <. G , R >. ) = <. ( ( 1st ` <. F , Q >. ) o. ( 1st ` <. G , R >. ) ) , ( ( 2nd ` <. F , Q >. ) .+^ ( 2nd ` <. G , R >. ) ) >. )
15 op1stg 
 |-  ( ( F e. T /\ Q e. E ) -> ( 1st ` <. F , Q >. ) = F )
16 15 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( 1st ` <. F , Q >. ) = F )
17 op1stg 
 |-  ( ( G e. T /\ R e. E ) -> ( 1st ` <. G , R >. ) = G )
18 17 3ad2ant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( 1st ` <. G , R >. ) = G )
19 16 18 coeq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( ( 1st ` <. F , Q >. ) o. ( 1st ` <. G , R >. ) ) = ( F o. G ) )
20 op2ndg 
 |-  ( ( F e. T /\ Q e. E ) -> ( 2nd ` <. F , Q >. ) = Q )
21 20 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( 2nd ` <. F , Q >. ) = Q )
22 op2ndg 
 |-  ( ( G e. T /\ R e. E ) -> ( 2nd ` <. G , R >. ) = R )
23 22 3ad2ant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( 2nd ` <. G , R >. ) = R )
24 21 23 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( ( 2nd ` <. F , Q >. ) .+^ ( 2nd ` <. G , R >. ) ) = ( Q .+^ R ) )
25 19 24 opeq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> <. ( ( 1st ` <. F , Q >. ) o. ( 1st ` <. G , R >. ) ) , ( ( 2nd ` <. F , Q >. ) .+^ ( 2nd ` <. G , R >. ) ) >. = <. ( F o. G ) , ( Q .+^ R ) >. )
26 14 25 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+ <. G , R >. ) = <. ( F o. G ) , ( Q .+^ R ) >. )