Metamath Proof Explorer


Theorem erngdvlem1-rN

Description: Lemma for eringring . (Contributed by NM, 4-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
Assertion erngdvlem1-rN K HL W H D Grp

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 eqid Base D = Base D
10 1 4 5 2 9 erngbase-rN K HL W H Base D = E
11 10 eqcomd K HL W H E = Base D
12 eqid + D = + D
13 1 4 5 2 12 erngfplus-rN 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 s P t E
16 1 4 5 6 tendoplass K HL W H s E t E u E s P t P u = s P t P u
17 3 1 4 5 7 tendo0cl K HL W H O E
18 3 1 4 5 7 6 tendo0pl K HL W H s E O P s = 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 s P s = O
21 11 14 15 16 17 18 19 20 isgrpd K HL W H D Grp