This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvhvaddcomN

Description: Commutativity of vector sum. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014) (New usage is discouraged.)

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 dvhvaddcomN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = ( G .+ F ) )

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 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( K e. HL /\ W e. H ) )
9 xp1st 
 |-  ( F e. ( T X. E ) -> ( 1st ` F ) e. T )
10 9 ad2antrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( 1st ` F ) e. T )
11 xp1st 
 |-  ( G e. ( T X. E ) -> ( 1st ` G ) e. T )
12 11 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( 1st ` G ) e. T )
13 1 2 ltrncom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 1st ` F ) e. T /\ ( 1st ` G ) e. T ) -> ( ( 1st ` F ) o. ( 1st ` G ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
14 8 10 12 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 1st ` F ) o. ( 1st ` G ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
15 xp2nd 
 |-  ( F e. ( T X. E ) -> ( 2nd ` F ) e. E )
16 xp2nd 
 |-  ( G e. ( T X. E ) -> ( 2nd ` G ) e. E )
17 15 16 anim12i 
 |-  ( ( F e. ( T X. E ) /\ G e. ( T X. E ) ) -> ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E ) )
18 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 ) ) ) )
19 1 2 3 18 tendoplcom 
 |-  ( ( ( 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 ) ) = ( ( 2nd ` G ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` F ) ) )
20 19 3expb 
 |-  ( ( ( 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 ) ) = ( ( 2nd ` G ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` F ) ) )
21 17 20 sylan2 
 |-  ( ( ( 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 ) ) = ( ( 2nd ` G ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` F ) ) )
22 1 2 3 4 5 18 6 dvhfplusr 
 |-  ( ( K e. HL /\ W e. H ) -> .+^ = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) )
23 22 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 ) ) ) ) )
24 23 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 ) ) )
25 23 oveqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 2nd ` G ) .+^ ( 2nd ` F ) ) = ( ( 2nd ` G ) ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) ( 2nd ` F ) ) )
26 21 24 25 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) = ( ( 2nd ` G ) .+^ ( 2nd ` F ) ) )
27 14 26 opeq12d 
 |-  ( ( ( 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 ` G ) o. ( 1st ` F ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` F ) ) >. )
28 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 ) ) >. )
29 1 2 3 4 5 7 6 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. ( T X. E ) /\ F e. ( T X. E ) ) ) -> ( G .+ F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` F ) ) >. )
30 29 ancom2s 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( G .+ F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` F ) ) >. )
31 27 28 30 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = ( G .+ F ) )