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