Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemn4.b |
|- B = ( Base ` K ) |
2 |
|
cdlemn4.l |
|- .<_ = ( le ` K ) |
3 |
|
cdlemn4.a |
|- A = ( Atoms ` K ) |
4 |
|
cdlemn4.p |
|- P = ( ( oc ` K ) ` W ) |
5 |
|
cdlemn4.h |
|- H = ( LHyp ` K ) |
6 |
|
cdlemn4.t |
|- T = ( ( LTrn ` K ) ` W ) |
7 |
|
cdlemn4.o |
|- O = ( h e. T |-> ( _I |` B ) ) |
8 |
|
cdlemn4.u |
|- U = ( ( DVecH ` K ) ` W ) |
9 |
|
cdlemn4.f |
|- F = ( iota_ h e. T ( h ` P ) = Q ) |
10 |
|
cdlemn4.g |
|- G = ( iota_ h e. T ( h ` P ) = R ) |
11 |
|
cdlemn4.j |
|- J = ( iota_ h e. T ( h ` Q ) = R ) |
12 |
|
cdlemn4.s |
|- .+ = ( +g ` U ) |
13 |
|
simp1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( K e. HL /\ W e. H ) ) |
14 |
2 3 5 4
|
lhpocnel2 |
|- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) ) |
15 |
13 14
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) ) |
16 |
|
simp2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) ) |
17 |
2 3 5 6 9
|
ltrniotacl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> F e. T ) |
18 |
13 15 16 17
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> F e. T ) |
19 |
|
eqid |
|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W ) |
20 |
5 6 19
|
tendoidcl |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) |
21 |
13 20
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) |
22 |
2 3 5 6 11
|
ltrniotacl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> J e. T ) |
23 |
1 5 6 19 7
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> O e. ( ( TEndo ` K ) ` W ) ) |
24 |
13 23
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> O e. ( ( TEndo ` K ) ` W ) ) |
25 |
|
eqid |
|- ( Scalar ` U ) = ( Scalar ` U ) |
26 |
|
eqid |
|- ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) ) |
27 |
5 6 19 8 25 12 26
|
dvhopvadd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) /\ ( J e. T /\ O e. ( ( TEndo ` K ) ` W ) ) ) -> ( <. F , ( _I |` T ) >. .+ <. J , O >. ) = <. ( F o. J ) , ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) >. ) |
28 |
13 18 21 22 24 27
|
syl122anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( <. F , ( _I |` T ) >. .+ <. J , O >. ) = <. ( F o. J ) , ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) >. ) |
29 |
5 6
|
ltrncom |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ J e. T ) -> ( F o. J ) = ( J o. F ) ) |
30 |
13 18 22 29
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( F o. J ) = ( J o. F ) ) |
31 |
2 3 4 5 6 9 10 11
|
cdlemn3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J o. F ) = G ) |
32 |
30 31
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( F o. J ) = G ) |
33 |
|
eqid |
|- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W ) |
34 |
5 33 8 25
|
dvhsca |
|- ( ( K e. HL /\ W e. H ) -> ( Scalar ` U ) = ( ( EDRing ` K ) ` W ) ) |
35 |
34
|
fveq2d |
|- ( ( K e. HL /\ W e. H ) -> ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) ) ) |
36 |
|
eqid |
|- ( 0g ` ( ( EDRing ` K ) ` W ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) ) |
37 |
1 5 6 33 7 36
|
erng0g |
|- ( ( K e. HL /\ W e. H ) -> ( 0g ` ( ( EDRing ` K ) ` W ) ) = O ) |
38 |
35 37
|
eqtrd |
|- ( ( K e. HL /\ W e. H ) -> ( 0g ` ( Scalar ` U ) ) = O ) |
39 |
13 38
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( 0g ` ( Scalar ` U ) ) = O ) |
40 |
39
|
oveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) ( 0g ` ( Scalar ` U ) ) ) = ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) ) |
41 |
5 33
|
erngdv |
|- ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing ) |
42 |
|
drnggrp |
|- ( ( ( EDRing ` K ) ` W ) e. DivRing -> ( ( EDRing ` K ) ` W ) e. Grp ) |
43 |
41 42
|
syl |
|- ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. Grp ) |
44 |
34 43
|
eqeltrd |
|- ( ( K e. HL /\ W e. H ) -> ( Scalar ` U ) e. Grp ) |
45 |
13 44
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Scalar ` U ) e. Grp ) |
46 |
|
eqid |
|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) ) |
47 |
5 19 8 25 46
|
dvhbase |
|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) ) |
48 |
13 47
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) ) |
49 |
21 48
|
eleqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( _I |` T ) e. ( Base ` ( Scalar ` U ) ) ) |
50 |
|
eqid |
|- ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) ) |
51 |
46 26 50
|
grprid |
|- ( ( ( Scalar ` U ) e. Grp /\ ( _I |` T ) e. ( Base ` ( Scalar ` U ) ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) ( 0g ` ( Scalar ` U ) ) ) = ( _I |` T ) ) |
52 |
45 49 51
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) ( 0g ` ( Scalar ` U ) ) ) = ( _I |` T ) ) |
53 |
40 52
|
eqtr3d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) = ( _I |` T ) ) |
54 |
32 53
|
opeq12d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. ( F o. J ) , ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) >. = <. G , ( _I |` T ) >. ) |
55 |
28 54
|
eqtr2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. G , ( _I |` T ) >. = ( <. F , ( _I |` T ) >. .+ <. J , O >. ) ) |