Step |
Hyp |
Ref |
Expression |
1 |
|
ernggrp.h |
|- H = ( LHyp ` K ) |
2 |
|
ernggrp.d |
|- D = ( ( EDRing ` K ) ` W ) |
3 |
|
erngdv.b |
|- B = ( Base ` K ) |
4 |
|
erngdv.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
erngdv.e |
|- E = ( ( TEndo ` K ) ` W ) |
6 |
|
erngdv.p |
|- P = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) |
7 |
|
erngdv.o |
|- .0. = ( f e. T |-> ( _I |` B ) ) |
8 |
|
erngdv.i |
|- I = ( a e. E |-> ( f e. T |-> `' ( a ` f ) ) ) |
9 |
|
erngrnglem.m |
|- .+ = ( a e. E , b e. E |-> ( a o. b ) ) |
10 |
|
edlemk6.j |
|- .\/ = ( join ` K ) |
11 |
|
edlemk6.m |
|- ./\ = ( meet ` K ) |
12 |
|
edlemk6.r |
|- R = ( ( trL ` K ) ` W ) |
13 |
|
edlemk6.p |
|- Q = ( ( oc ` K ) ` W ) |
14 |
|
edlemk6.z |
|- Z = ( ( Q .\/ ( R ` b ) ) ./\ ( ( h ` Q ) .\/ ( R ` ( b o. `' ( s ` h ) ) ) ) ) |
15 |
|
edlemk6.y |
|- Y = ( ( Q .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) ) |
16 |
|
edlemk6.x |
|- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` ( s ` h ) ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` Q ) = Y ) ) |
17 |
|
edlemk6.u |
|- U = ( g e. T |-> if ( ( s ` h ) = h , g , X ) ) |
18 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
19 |
1 4 5 2 18
|
erngbase |
|- ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E ) |
20 |
19
|
eqcomd |
|- ( ( K e. HL /\ W e. H ) -> E = ( Base ` D ) ) |
21 |
20
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> E = ( Base ` D ) ) |
22 |
|
eqid |
|- ( .r ` D ) = ( .r ` D ) |
23 |
1 4 5 2 22
|
erngfmul |
|- ( ( K e. HL /\ W e. H ) -> ( .r ` D ) = ( a e. E , b e. E |-> ( a o. b ) ) ) |
24 |
9 23
|
eqtr4id |
|- ( ( K e. HL /\ W e. H ) -> .+ = ( .r ` D ) ) |
25 |
24
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> .+ = ( .r ` D ) ) |
26 |
3 1 4 5 7
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> .0. e. E ) |
27 |
26 19
|
eleqtrrd |
|- ( ( K e. HL /\ W e. H ) -> .0. e. ( Base ` D ) ) |
28 |
|
eqid |
|- ( +g ` D ) = ( +g ` D ) |
29 |
1 4 5 2 28
|
erngfplus |
|- ( ( K e. HL /\ W e. H ) -> ( +g ` D ) = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) ) |
30 |
6 29
|
eqtr4id |
|- ( ( K e. HL /\ W e. H ) -> P = ( +g ` D ) ) |
31 |
30
|
oveqd |
|- ( ( K e. HL /\ W e. H ) -> ( .0. P .0. ) = ( .0. ( +g ` D ) .0. ) ) |
32 |
3 1 4 5 7 6
|
tendo0pl |
|- ( ( ( K e. HL /\ W e. H ) /\ .0. e. E ) -> ( .0. P .0. ) = .0. ) |
33 |
26 32
|
mpdan |
|- ( ( K e. HL /\ W e. H ) -> ( .0. P .0. ) = .0. ) |
34 |
31 33
|
eqtr3d |
|- ( ( K e. HL /\ W e. H ) -> ( .0. ( +g ` D ) .0. ) = .0. ) |
35 |
1 2 3 4 5 6 7 8
|
erngdvlem1 |
|- ( ( K e. HL /\ W e. H ) -> D e. Grp ) |
36 |
|
eqid |
|- ( 0g ` D ) = ( 0g ` D ) |
37 |
18 28 36
|
isgrpid2 |
|- ( D e. Grp -> ( ( .0. e. ( Base ` D ) /\ ( .0. ( +g ` D ) .0. ) = .0. ) <-> ( 0g ` D ) = .0. ) ) |
38 |
35 37
|
syl |
|- ( ( K e. HL /\ W e. H ) -> ( ( .0. e. ( Base ` D ) /\ ( .0. ( +g ` D ) .0. ) = .0. ) <-> ( 0g ` D ) = .0. ) ) |
39 |
27 34 38
|
mpbi2and |
|- ( ( K e. HL /\ W e. H ) -> ( 0g ` D ) = .0. ) |
40 |
39
|
eqcomd |
|- ( ( K e. HL /\ W e. H ) -> .0. = ( 0g ` D ) ) |
41 |
40
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> .0. = ( 0g ` D ) ) |
42 |
1 2 3 4 5 6 7 8 9
|
erngdvlem3 |
|- ( ( K e. HL /\ W e. H ) -> D e. Ring ) |
43 |
1 4 5 2 42
|
erng1lem |
|- ( ( K e. HL /\ W e. H ) -> ( 1r ` D ) = ( _I |` T ) ) |
44 |
43
|
eqcomd |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) = ( 1r ` D ) ) |
45 |
44
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> ( _I |` T ) = ( 1r ` D ) ) |
46 |
42
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> D e. Ring ) |
47 |
|
simp1l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( K e. HL /\ W e. H ) ) |
48 |
24
|
oveqd |
|- ( ( K e. HL /\ W e. H ) -> ( s .+ t ) = ( s ( .r ` D ) t ) ) |
49 |
47 48
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( s .+ t ) = ( s ( .r ` D ) t ) ) |
50 |
|
simp2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> s e. E ) |
51 |
|
simp3l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> t e. E ) |
52 |
1 4 5 2 22
|
erngmul |
|- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E ) ) -> ( s ( .r ` D ) t ) = ( s o. t ) ) |
53 |
47 50 51 52
|
syl12anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( s ( .r ` D ) t ) = ( s o. t ) ) |
54 |
49 53
|
eqtrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( s .+ t ) = ( s o. t ) ) |
55 |
3 1 4 5 7
|
tendoconid |
|- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( s o. t ) =/= .0. ) |
56 |
55
|
3adant1r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( s o. t ) =/= .0. ) |
57 |
54 56
|
eqnetrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) /\ ( t e. E /\ t =/= .0. ) ) -> ( s .+ t ) =/= .0. ) |
58 |
3 1 4 5 7
|
tendo1ne0 |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) =/= .0. ) |
59 |
58
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> ( _I |` T ) =/= .0. ) |
60 |
|
simpll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( K e. HL /\ W e. H ) ) |
61 |
|
simplrl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> h e. T ) |
62 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( s e. E /\ s =/= .0. ) ) |
63 |
3 10 11 1 4 12 13 14 15 16 17 5 7
|
cdleml6 |
|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> ( U e. E /\ ( U ` ( s ` h ) ) = h ) ) |
64 |
63
|
simpld |
|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> U e. E ) |
65 |
60 61 62 64
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> U e. E ) |
66 |
3 10 11 1 4 12 13 14 15 16 17 5 7
|
cdleml9 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) /\ ( s e. E /\ s =/= .0. ) ) -> U =/= .0. ) |
67 |
66
|
3expa |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> U =/= .0. ) |
68 |
24
|
oveqd |
|- ( ( K e. HL /\ W e. H ) -> ( U .+ s ) = ( U ( .r ` D ) s ) ) |
69 |
68
|
ad2antrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( U .+ s ) = ( U ( .r ` D ) s ) ) |
70 |
|
simprl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> s e. E ) |
71 |
1 4 5 2 22
|
erngmul |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ s e. E ) ) -> ( U ( .r ` D ) s ) = ( U o. s ) ) |
72 |
60 65 70 71
|
syl12anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( U ( .r ` D ) s ) = ( U o. s ) ) |
73 |
3 10 11 1 4 12 13 14 15 16 17 5 7
|
cdleml8 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( U o. s ) = ( _I |` T ) ) |
74 |
73
|
3expa |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( U o. s ) = ( _I |` T ) ) |
75 |
69 72 74
|
3eqtrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) /\ ( s e. E /\ s =/= .0. ) ) -> ( U .+ s ) = ( _I |` T ) ) |
76 |
21 25 41 45 46 57 59 65 67 75
|
isdrngd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( h e. T /\ h =/= ( _I |` B ) ) ) -> D e. DivRing ) |