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