Metamath Proof Explorer

Theorem erngdvlem3-rN

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

Ref Expression
Hypotheses ernggrp.h-r ⊢H=LHyp⁡K
ernggrp.d-r ⊢D=EDRingR⁡K⁡W
ernggrplem.b-r ⊢B=BaseK
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
Assertion erngdvlem3-rN ⊢K∈HL∧W∈H→D∈Ring

Proof

Step Hyp Ref Expression
1 ernggrp.h-r ⊢H=LHyp⁡K
2 ernggrp.d-r ⊢D=EDRingR⁡K⁡W
3 ernggrplem.b-r ⊢B=BaseK
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 eqid ⊢BaseD=BaseD
11 1 4 5 2 10 erngbase-rN ⊢K∈HL∧W∈H→BaseD=E
12 11 eqcomd ⊢K∈HL∧W∈H→E=BaseD
13 eqid ⊢+D=+D
14 1 4 5 2 13 erngfplus-rN ⊢K∈HL∧W∈H→+D=a∈E,b∈E⟼f∈T⟼a⁡f∘b⁡f
15 6 14 eqtr4id ⊢K∈HL∧W∈H→P=+D
16 eqid ⊢⋅D=⋅D
17 1 4 5 2 16 erngfmul-rN ⊢K∈HL∧W∈H→⋅D=a∈E,b∈E⟼b∘a
18 9 17 eqtr4id ⊢K∈HL∧W∈H→M=⋅D
19 1 2 3 4 5 6 7 8 erngdvlem1-rN ⊢K∈HL∧W∈H→D∈Grp
20 18 oveqd ⊢K∈HL∧W∈H→sMt=s⋅Dt
21 20 3ad2ant1 ⊢K∈HL∧W∈H∧s∈E∧t∈E→sMt=s⋅Dt
22 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧s∈E∧t∈E→s⋅Dt=t∘s
23 22 3impb ⊢K∈HL∧W∈H∧s∈E∧t∈E→s⋅Dt=t∘s
24 21 23 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E→sMt=t∘s
25 1 5 tendococl ⊢K∈HL∧W∈H∧t∈E∧s∈E→t∘s∈E
26 25 3com23 ⊢K∈HL∧W∈H∧s∈E∧t∈E→t∘s∈E
27 24 26 eqeltrd ⊢K∈HL∧W∈H∧s∈E∧t∈E→sMt∈E
28 18 oveqdr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→tMu=t⋅Du
29 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧t∈E∧u∈E→t⋅Du=u∘t
30 29 3adantr1 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→t⋅Du=u∘t
31 28 30 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→tMu=u∘t
32 31 coeq1d ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→tMu∘s=u∘t∘s
33 18 oveqd ⊢K∈HL∧W∈H→sMtMu=s⋅DtMu
34 33 adantr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtMu=s⋅DtMu
35 simpl ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→K∈HL∧W∈H
36 simpr1 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→s∈E
37 simpr3 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→u∈E
38 simpr2 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→t∈E
39 1 5 tendococl ⊢K∈HL∧W∈H∧u∈E∧t∈E→u∘t∈E
40 35 37 38 39 syl3anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→u∘t∈E
41 31 40 eqeltrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→tMu∈E
42 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧s∈E∧tMu∈E→s⋅DtMu=tMu∘s
43 35 36 41 42 syl12anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→s⋅DtMu=tMu∘s
44 34 43 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtMu=tMu∘s
45 18 oveqd ⊢K∈HL∧W∈H→sMtMu=sMt⋅Du
46 45 adantr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtMu=sMt⋅Du
47 27 3adant3r3 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMt∈E
48 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧sMt∈E∧u∈E→sMt⋅Du=u∘sMt
49 35 47 37 48 syl12anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMt⋅Du=u∘sMt
50 18 oveqdr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMt=s⋅Dt
51 22 3adantr3 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→s⋅Dt=t∘s
52 50 51 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMt=t∘s
53 52 coeq2d ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→u∘sMt=u∘t∘s
54 46 49 53 3eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtMu=u∘t∘s
55 coass ⊢u∘t∘s=u∘t∘s
56 54 55 eqtr4di ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtMu=u∘t∘s
57 32 44 56 3eqtr4rd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtMu=sMtMu
58 1 4 5 6 tendodi2 ⊢K∈HL∧W∈H∧t∈E∧u∈E∧s∈E→tPu∘s=t∘sPu∘s
59 35 38 37 36 58 syl13anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→tPu∘s=t∘sPu∘s
60 18 oveqd ⊢K∈HL∧W∈H→sMtPu=s⋅DtPu
61 60 adantr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtPu=s⋅DtPu
62 1 4 5 6 tendoplcl ⊢K∈HL∧W∈H∧t∈E∧u∈E→tPu∈E
63 35 38 37 62 syl3anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→tPu∈E
64 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧s∈E∧tPu∈E→s⋅DtPu=tPu∘s
65 35 36 63 64 syl12anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→s⋅DtPu=tPu∘s
66 61 65 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtPu=tPu∘s
67 18 oveqdr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMu=s⋅Du
68 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧s∈E∧u∈E→s⋅Du=u∘s
69 68 3adantr2 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→s⋅Du=u∘s
70 67 69 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMu=u∘s
71 52 70 oveq12d ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtPsMu=t∘sPu∘s
72 59 66 71 3eqtr4d ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMtPu=sMtPsMu
73 1 4 5 6 tendodi1 ⊢K∈HL∧W∈H∧u∈E∧s∈E∧t∈E→u∘sPt=u∘sPu∘t
74 35 37 36 38 73 syl13anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→u∘sPt=u∘sPu∘t
75 18 adantr ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→M=⋅D
76 75 oveqd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sPtMu=sPt⋅Du
77 1 4 5 6 tendoplcl ⊢K∈HL∧W∈H∧s∈E∧t∈E→sPt∈E
78 77 3adant3r3 ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sPt∈E
79 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧sPt∈E∧u∈E→sPt⋅Du=u∘sPt
80 35 78 37 79 syl12anc ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sPt⋅Du=u∘sPt
81 76 80 eqtrd ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sPtMu=u∘sPt
82 70 31 oveq12d ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sMuPtMu=u∘sPu∘t
83 74 81 82 3eqtr4d ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sPtMu=sMuPtMu
84 1 4 5 tendoidcl ⊢K∈HL∧W∈H→I↾T∈E
85 18 oveqd ⊢K∈HL∧W∈H→I↾TMs=I↾T⋅Ds
86 85 adantr ⊢K∈HL∧W∈H∧s∈E→I↾TMs=I↾T⋅Ds
87 simpl ⊢K∈HL∧W∈H∧s∈E→K∈HL∧W∈H
88 84 adantr ⊢K∈HL∧W∈H∧s∈E→I↾T∈E
89 simpr ⊢K∈HL∧W∈H∧s∈E→s∈E
90 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧I↾T∈E∧s∈E→I↾T⋅Ds=s∘I↾T
91 87 88 89 90 syl12anc ⊢K∈HL∧W∈H∧s∈E→I↾T⋅Ds=s∘I↾T
92 1 4 5 tendo1mulr ⊢K∈HL∧W∈H∧s∈E→s∘I↾T=s
93 86 91 92 3eqtrd ⊢K∈HL∧W∈H∧s∈E→I↾TMs=s
94 18 oveqd ⊢K∈HL∧W∈H→sMI↾T=s⋅DI↾T
95 94 adantr ⊢K∈HL∧W∈H∧s∈E→sMI↾T=s⋅DI↾T
96 1 4 5 2 16 erngmul-rN ⊢K∈HL∧W∈H∧s∈E∧I↾T∈E→s⋅DI↾T=I↾T∘s
97 87 89 88 96 syl12anc ⊢K∈HL∧W∈H∧s∈E→s⋅DI↾T=I↾T∘s
98 1 4 5 tendo1mul ⊢K∈HL∧W∈H∧s∈E→I↾T∘s=s
99 95 97 98 3eqtrd ⊢K∈HL∧W∈H∧s∈E→sMI↾T=s
100 12 15 18 19 27 57 72 83 84 93 99 isringd ⊢K∈HL∧W∈H→D∈Ring