Metamath Proof Explorer


Theorem erngdvlem4-rN

Description: Lemma for erngdv . (Contributed by NM, 11-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ernggrp.h-r H = LHyp K
ernggrp.d-r D = EDRing R K W
ernggrplem.b-r B = Base K
ernggrplem.t-r T = LTrn K W
ernggrplem.e-r E = TEndo K W
ernggrplem.p-r P = a E , b E f T a f b f
ernggrplem.o-r O = f T I B
ernggrplem.i-r I = a E f T a f -1
erngrnglem.m-r M = a E , b E b a
edlemk6.j-r ˙ = join K
edlemk6.m-r ˙ = meet K
edlemk6.r-r R = trL K W
edlemk6.p-r Q = oc K W
edlemk6.z-r Z = Q ˙ R b ˙ h Q ˙ R b s h -1
edlemk6.y-r Y = Q ˙ R g ˙ Z ˙ R g b -1
edlemk6.x-r X = ι z T | b T b I B R b R s h R b R g z Q = Y
edlemk6.u-r U = g T if s h = h g X
Assertion erngdvlem4-rN K HL W H h T h I B D DivRing

Proof

Step Hyp Ref Expression
1 ernggrp.h-r H = LHyp K
2 ernggrp.d-r D = EDRing R K W
3 ernggrplem.b-r B = Base K
4 ernggrplem.t-r T = LTrn K W
5 ernggrplem.e-r E = TEndo K W
6 ernggrplem.p-r P = a E , b E f T a f b f
7 ernggrplem.o-r O = f T I B
8 ernggrplem.i-r I = a E f T a f -1
9 erngrnglem.m-r M = a E , b E b a
10 edlemk6.j-r ˙ = join K
11 edlemk6.m-r ˙ = meet K
12 edlemk6.r-r R = trL K W
13 edlemk6.p-r Q = oc K W
14 edlemk6.z-r Z = Q ˙ R b ˙ h Q ˙ R b s h -1
15 edlemk6.y-r Y = Q ˙ R g ˙ Z ˙ R g b -1
16 edlemk6.x-r X = ι z T | b T b I B R b R s h R b R g z Q = Y
17 edlemk6.u-r U = g T if s h = h g X
18 eqid Base D = Base D
19 1 4 5 2 18 erngbase-rN K HL W H Base D = E
20 19 eqcomd K HL W H E = Base D
21 20 adantr K HL W H h T h I B E = Base D
22 eqid D = D
23 1 4 5 2 22 erngfmul-rN K HL W H D = a E , b E b a
24 9 23 eqtr4id K HL W H M = D
25 24 adantr K HL W H h T h I B M = D
26 3 1 4 5 7 tendo0cl K HL W H O E
27 26 19 eleqtrrd K HL W H O Base D
28 eqid + D = + D
29 1 4 5 2 28 erngfplus-rN K HL W H + D = a E , b E f T a f b f
30 6 29 eqtr4id K HL W H P = + D
31 30 oveqd K HL W H O P O = O + D O
32 3 1 4 5 7 6 tendo0pl K HL W H O E O P O = O
33 26 32 mpdan K HL W H O P O = O
34 31 33 eqtr3d K HL W H O + D O = O
35 1 2 3 4 5 6 7 8 erngdvlem1-rN K HL W H D Grp
36 eqid 0 D = 0 D
37 18 28 36 isgrpid2 D Grp O Base D O + D O = O 0 D = O
38 35 37 syl K HL W H O Base D O + D O = O 0 D = O
39 27 34 38 mpbi2and K HL W H 0 D = O
40 39 eqcomd K HL W H O = 0 D
41 40 adantr K HL W H h T h I B O = 0 D
42 1 4 5 tendoidcl K HL W H I T E
43 42 19 eleqtrrd K HL W H I T Base D
44 19 eleq2d K HL W H u Base D u E
45 simpl K HL W H u E K HL W H
46 42 adantr K HL W H u E I T E
47 simpr K HL W H u E u E
48 1 4 5 2 22 erngmul-rN K HL W H I T E u E I T D u = u I T
49 45 46 47 48 syl12anc K HL W H u E I T D u = u I T
50 1 4 5 tendo1mulr K HL W H u E u I T = u
51 49 50 eqtrd K HL W H u E I T D u = u
52 1 4 5 2 22 erngmul-rN K HL W H u E I T E u D I T = I T u
53 45 47 46 52 syl12anc K HL W H u E u D I T = I T u
54 1 4 5 tendo1mul K HL W H u E I T u = u
55 53 54 eqtrd K HL W H u E u D I T = u
56 51 55 jca K HL W H u E I T D u = u u D I T = u
57 56 ex K HL W H u E I T D u = u u D I T = u
58 44 57 sylbid K HL W H u Base D I T D u = u u D I T = u
59 58 ralrimiv K HL W H u Base D I T D u = u u D I T = u
60 1 2 3 4 5 6 7 8 9 erngdvlem3-rN K HL W H D Ring
61 eqid 1 D = 1 D
62 18 22 61 isringid D Ring I T Base D u Base D I T D u = u u D I T = u 1 D = I T
63 60 62 syl K HL W H I T Base D u Base D I T D u = u u D I T = u 1 D = I T
64 43 59 63 mpbi2and K HL W H 1 D = I T
65 64 eqcomd K HL W H I T = 1 D
66 65 adantr K HL W H h T h I B I T = 1 D
67 60 adantr K HL W H h T h I B D Ring
68 simp1l K HL W H h T h I B s E s O t E t O K HL W H
69 24 oveqd K HL W H s M t = s D t
70 68 69 syl K HL W H h T h I B s E s O t E t O s M t = s D t
71 simp2l K HL W H h T h I B s E s O t E t O s E
72 simp3l K HL W H h T h I B s E s O t E t O t E
73 1 4 5 2 22 erngmul-rN K HL W H s E t E s D t = t s
74 68 71 72 73 syl12anc K HL W H h T h I B s E s O t E t O s D t = t s
75 70 74 eqtrd K HL W H h T h I B s E s O t E t O s M t = t s
76 simp3 K HL W H h T h I B s E s O t E t O t E t O
77 simp2 K HL W H h T h I B s E s O t E t O s E s O
78 3 1 4 5 7 tendoconid K HL W H t E t O s E s O t s O
79 68 76 77 78 syl3anc K HL W H h T h I B s E s O t E t O t s O
80 75 79 eqnetrd K HL W H h T h I B s E s O t E t O s M t O
81 3 1 4 5 7 tendo1ne0 K HL W H I T O
82 81 adantr K HL W H h T h I B I T O
83 simpll K HL W H h T h I B s E s O K HL W H
84 simplrl K HL W H h T h I B s E s O h T
85 simpr K HL W H h T h I B s E s O s E s O
86 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml6 K HL W H h T s E s O U E U s h = h
87 86 simpld K HL W H h T s E s O U E
88 83 84 85 87 syl3anc K HL W H h T h I B s E s O U E
89 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml9 K HL W H h T h I B s E s O U O
90 89 3expa K HL W H h T h I B s E s O U O
91 24 oveqd K HL W H s M U = s D U
92 91 ad2antrr K HL W H h T h I B s E s O s M U = s D U
93 simprl K HL W H h T h I B s E s O s E
94 1 4 5 2 22 erngmul-rN K HL W H s E U E s D U = U s
95 83 93 88 94 syl12anc K HL W H h T h I B s E s O s D U = U s
96 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml8 K HL W H h T h I B s E s O U s = I T
97 96 3expa K HL W H h T h I B s E s O U s = I T
98 95 97 eqtrd K HL W H h T h I B s E s O s D U = I T
99 92 98 eqtrd K HL W H h T h I B s E s O s M U = I T
100 21 25 41 66 67 80 82 88 90 99 isdrngrd K HL W H h T h I B D DivRing