Metamath Proof Explorer

Theorem erngdvlem1

Description: Lemma for eringring . (Contributed by NM, 4-Aug-2013)

Ref Expression
Hypotheses ernggrp.h ⊢H=LHyp⁡K
ernggrp.d ⊢D=EDRing⁡K⁡W
erngdv.b ⊢B=BaseK
erngdv.t ⊢T=LTrn⁡K⁡W
erngdv.e ⊢E=TEndo⁡K⁡W
erngdv.p ⊢P=a∈E,b∈E⟼f∈T⟼a⁡f∘b⁡f
erngdv.o ⊢0˙=f∈T⟼I↾B
erngdv.i ⊢I=a∈E⟼f∈T⟼a⁡f-1
Assertion erngdvlem1 ⊢K∈HL∧W∈H→D∈Grp

Proof

Step Hyp Ref Expression
1 ernggrp.h ⊢H=LHyp⁡K
2 ernggrp.d ⊢D=EDRing⁡K⁡W
3 erngdv.b ⊢B=BaseK
4 erngdv.t ⊢T=LTrn⁡K⁡W
5 erngdv.e ⊢E=TEndo⁡K⁡W
6 erngdv.p ⊢P=a∈E,b∈E⟼f∈T⟼a⁡f∘b⁡f
7 erngdv.o ⊢0˙=f∈T⟼I↾B
8 erngdv.i ⊢I=a∈E⟼f∈T⟼a⁡f-1
9 eqid ⊢BaseD=BaseD
10 1 4 5 2 9 erngbase ⊢K∈HL∧W∈H→BaseD=E
11 10 eqcomd ⊢K∈HL∧W∈H→E=BaseD
12 eqid ⊢+D=+D
13 1 4 5 2 12 erngfplus ⊢K∈HL∧W∈H→+D=a∈E,b∈E⟼f∈T⟼a⁡f∘b⁡f
14 6 13 eqtr4id ⊢K∈HL∧W∈H→P=+D
15 1 4 5 6 tendoplcl ⊢K∈HL∧W∈H∧s∈E∧t∈E→sPt∈E
16 1 4 5 6 tendoplass ⊢K∈HL∧W∈H∧s∈E∧t∈E∧u∈E→sPtPu=sPtPu
17 3 1 4 5 7 tendo0cl ⊢K∈HL∧W∈H→0˙∈E
18 3 1 4 5 7 6 tendo0pl ⊢K∈HL∧W∈H∧s∈E→0˙Ps=s
19 1 4 5 8 tendoicl ⊢K∈HL∧W∈H∧s∈E→I⁡s∈E
20 1 4 5 8 3 6 7 tendoipl ⊢K∈HL∧W∈H∧s∈E→I⁡sPs=0˙
21 11 14 15 16 17 18 19 20 isgrpd ⊢K∈HL∧W∈H→D∈Grp