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 ) )