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