Metamath Proof Explorer

Theorem dvhvaddcl

Description: Closure of 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 dvhvaddcl.h 
|- H = ( LHyp ` K )
dvhvaddcl.t 
|- T = ( ( LTrn ` K ) ` W )
dvhvaddcl.e 
|- E = ( ( TEndo ` K ) ` W )
dvhvaddcl.u 
|- U = ( ( DVecH ` K ) ` W )
dvhvaddcl.d 
|- D = ( Scalar ` U )
dvhvaddcl.p 
|- .+^ = ( +g ` D )
dvhvaddcl.a 
|- .+ = ( +g ` U )
Assertion dvhvaddcl 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) )

Proof

Step Hyp Ref Expression
1 dvhvaddcl.h 
 |-  H = ( LHyp ` K )
2 dvhvaddcl.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhvaddcl.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhvaddcl.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dvhvaddcl.d 
 |-  D = ( Scalar ` U )
6 dvhvaddcl.p 
 |-  .+^ = ( +g ` D )
7 dvhvaddcl.a 
 |-  .+ = ( +g ` U )
8 1 2 3 4 5 7 6 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
9 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( K e. HL /\ W e. H ) )
10 xp1st 
 |-  ( F e. ( T X. E ) -> ( 1st ` F ) e. T )
11 10 ad2antrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( 1st ` F ) e. T )
12 xp1st 
 |-  ( G e. ( T X. E ) -> ( 1st ` G ) e. T )
13 12 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( 1st ` G ) e. T )
14 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 1st ` F ) e. T /\ ( 1st ` G ) e. T ) -> ( ( 1st ` F ) o. ( 1st ` G ) ) e. T )
15 9 11 13 14 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 1st ` F ) o. ( 1st ` G ) ) e. T )
16 eqid 
 |-  ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) )
17 1 2 3 4 5 16 6 dvhfplusr 
 |-  ( ( K e. HL /\ W e. H ) -> .+^ = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) )
18 17 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> .+^ = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) )
19 18 oveqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) = ( ( 2nd ` F ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` G ) ) )
20 xp2nd 
 |-  ( F e. ( T X. E ) -> ( 2nd ` F ) e. E )
21 20 ad2antrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( 2nd ` F ) e. E )
22 xp2nd 
 |-  ( G e. ( T X. E ) -> ( 2nd ` G ) e. E )
23 22 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( 2nd ` G ) e. E )
24 1 2 3 16 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E ) -> ( ( 2nd ` F ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` G ) ) e. E )
25 9 21 23 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 2nd ` F ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` G ) ) e. E )
26 19 25 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) e. E )
27 opelxpi 
 |-  ( ( ( ( 1st ` F ) o. ( 1st ` G ) ) e. T /\ ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) e. E ) -> <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. e. ( T X. E ) )
28 15 26 27 syl2anc 
 |-  ( ( ( 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 ) ) >. e. ( T X. E ) )
29 8 28 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) )