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 |
|
coass |
|- ( ( ( 1st ` F ) o. ( 1st ` G ) ) o. ( 1st ` I ) ) = ( ( 1st ` F ) o. ( ( 1st ` G ) o. ( 1st ` I ) ) ) |
9 |
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 ) ) >. ) |
10 |
9
|
3adantr3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) |
11 |
10
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( F .+ G ) ) = ( 1st ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) ) |
12 |
|
fvex |
|- ( 1st ` F ) e. _V |
13 |
|
fvex |
|- ( 1st ` G ) e. _V |
14 |
12 13
|
coex |
|- ( ( 1st ` F ) o. ( 1st ` G ) ) e. _V |
15 |
|
ovex |
|- ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) e. _V |
16 |
14 15
|
op1st |
|- ( 1st ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) = ( ( 1st ` F ) o. ( 1st ` G ) ) |
17 |
11 16
|
eqtrdi |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( F .+ G ) ) = ( ( 1st ` F ) o. ( 1st ` G ) ) ) |
18 |
17
|
coeq1d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) = ( ( ( 1st ` F ) o. ( 1st ` G ) ) o. ( 1st ` I ) ) ) |
19 |
1 2 3 4 5 7 6
|
dvhvadd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) = <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) |
20 |
19
|
3adantr1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) = <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) |
21 |
20
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( G .+ I ) ) = ( 1st ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) ) |
22 |
|
fvex |
|- ( 1st ` I ) e. _V |
23 |
13 22
|
coex |
|- ( ( 1st ` G ) o. ( 1st ` I ) ) e. _V |
24 |
|
ovex |
|- ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) e. _V |
25 |
23 24
|
op1st |
|- ( 1st ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) = ( ( 1st ` G ) o. ( 1st ` I ) ) |
26 |
21 25
|
eqtrdi |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( G .+ I ) ) = ( ( 1st ` G ) o. ( 1st ` I ) ) ) |
27 |
26
|
coeq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) = ( ( 1st ` F ) o. ( ( 1st ` G ) o. ( 1st ` I ) ) ) ) |
28 |
8 18 27
|
3eqtr4a |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) = ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) ) |
29 |
|
xp2nd |
|- ( F e. ( T X. E ) -> ( 2nd ` F ) e. E ) |
30 |
|
xp2nd |
|- ( G e. ( T X. E ) -> ( 2nd ` G ) e. E ) |
31 |
|
xp2nd |
|- ( I e. ( T X. E ) -> ( 2nd ` I ) e. E ) |
32 |
29 30 31
|
3anim123i |
|- ( ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) -> ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) |
33 |
|
eqid |
|- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W ) |
34 |
1 33 4 5
|
dvhsca |
|- ( ( K e. HL /\ W e. H ) -> D = ( ( EDRing ` K ) ` W ) ) |
35 |
1 33
|
erngdv |
|- ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing ) |
36 |
34 35
|
eqeltrd |
|- ( ( K e. HL /\ W e. H ) -> D e. DivRing ) |
37 |
|
drnggrp |
|- ( D e. DivRing -> D e. Grp ) |
38 |
36 37
|
syl |
|- ( ( K e. HL /\ W e. H ) -> D e. Grp ) |
39 |
38
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> D e. Grp ) |
40 |
|
simpr1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` F ) e. E ) |
41 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
42 |
1 3 4 5 41
|
dvhbase |
|- ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E ) |
43 |
42
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( Base ` D ) = E ) |
44 |
40 43
|
eleqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` F ) e. ( Base ` D ) ) |
45 |
|
simpr2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` G ) e. E ) |
46 |
45 43
|
eleqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` G ) e. ( Base ` D ) ) |
47 |
|
simpr3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` I ) e. E ) |
48 |
47 43
|
eleqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` I ) e. ( Base ` D ) ) |
49 |
41 6
|
grpass |
|- ( ( D e. Grp /\ ( ( 2nd ` F ) e. ( Base ` D ) /\ ( 2nd ` G ) e. ( Base ` D ) /\ ( 2nd ` I ) e. ( Base ` D ) ) ) -> ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) ) |
50 |
39 44 46 48 49
|
syl13anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) ) |
51 |
32 50
|
sylan2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) ) |
52 |
10
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( F .+ G ) ) = ( 2nd ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) ) |
53 |
14 15
|
op2nd |
|- ( 2nd ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) = ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) |
54 |
52 53
|
eqtrdi |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( F .+ G ) ) = ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) ) |
55 |
54
|
oveq1d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) = ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) ) |
56 |
20
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( G .+ I ) ) = ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) ) |
57 |
23 24
|
op2nd |
|- ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) = ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) |
58 |
56 57
|
eqtrdi |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( G .+ I ) ) = ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) |
59 |
58
|
oveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) ) |
60 |
51 55 59
|
3eqtr4d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) ) |
61 |
28 60
|
opeq12d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> <. ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) , ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) >. = <. ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) >. ) |
62 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( K e. HL /\ W e. H ) ) |
63 |
1 2 3 4 5 6 7
|
dvhvaddcl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) ) |
64 |
63
|
3adantr3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) ) |
65 |
|
simpr3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> I e. ( T X. E ) ) |
66 |
1 2 3 4 5 7 6
|
dvhvadd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( F .+ G ) e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = <. ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) , ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) >. ) |
67 |
62 64 65 66
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = <. ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) , ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) >. ) |
68 |
|
simpr1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> F e. ( T X. E ) ) |
69 |
1 2 3 4 5 6 7
|
dvhvaddcl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) e. ( T X. E ) ) |
70 |
69
|
3adantr1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) e. ( T X. E ) ) |
71 |
1 2 3 4 5 7 6
|
dvhvadd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ ( G .+ I ) e. ( T X. E ) ) ) -> ( F .+ ( G .+ I ) ) = <. ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) >. ) |
72 |
62 68 70 71
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( F .+ ( G .+ I ) ) = <. ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) >. ) |
73 |
61 67 72
|
3eqtr4d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = ( F .+ ( G .+ I ) ) ) |