Metamath Proof Explorer


Theorem erngdvlem2N

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

Ref Expression
Hypotheses ernggrp.h H = LHyp K
ernggrp.d D = EDRing K W
erngdv.b B = Base K
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 erngdvlem2N K HL W H D Abel

Proof

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 , 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 Base D = Base D
10 1 4 5 2 9 erngbase 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 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 2 3 4 5 6 7 8 erngdvlem1 K HL W H D Grp
16 1 4 5 6 tendoplcom K HL W H s E t E s P t = t P s
17 11 14 15 16 isabld K HL W H D Abel