Metamath Proof Explorer

Theorem erng0g

Description: The division ring zero of an endomorphism ring. (Contributed by NM, 5-Nov-2013) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses erng0g.b ⊢ B = Base K
erng0g.h ⊢ H = LHyp ⁡ K
erng0g.t ⊢ T = LTrn ⁡ K ⁡ W
erng0g.d ⊢ D = EDRing ⁡ K ⁡ W
erng0g.o ⊢ O = f ∈ T ⟼ I ↾ B
erng0g.z ⊢ 0 ˙ = 0 D
Assertion erng0g ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ = O

Proof

Step Hyp Ref Expression
1 erng0g.b ⊢ B = Base K
2 erng0g.h ⊢ H = LHyp ⁡ K
3 erng0g.t ⊢ T = LTrn ⁡ K ⁡ W
4 erng0g.d ⊢ D = EDRing ⁡ K ⁡ W
5 erng0g.o ⊢ O = f ∈ T ⟼ I ↾ B
6 erng0g.z ⊢ 0 ˙ = 0 D
7 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
8 eqid ⊢ + D = + D
9 2 3 7 4 8 erngfplus ⊢ K ∈ HL ∧ W ∈ H → + D = s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
10 9 oveqd ⊢ K ∈ HL ∧ W ∈ H → O + D O = O s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f O
11 1 2 3 7 5 tendo0cl ⊢ K ∈ HL ∧ W ∈ H → O ∈ TEndo ⁡ K ⁡ W
12 eqid ⊢ s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f = s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
13 1 2 3 7 5 12 tendo0pl ⊢ K ∈ HL ∧ W ∈ H ∧ O ∈ TEndo ⁡ K ⁡ W → O s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f O = O
14 11 13 mpdan ⊢ K ∈ HL ∧ W ∈ H → O s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f O = O
15 10 14 eqtrd ⊢ K ∈ HL ∧ W ∈ H → O + D O = O
16 2 4 eringring ⊢ K ∈ HL ∧ W ∈ H → D ∈ Ring
17 ringgrp ⊢ D ∈ Ring → D ∈ Grp
18 16 17 syl ⊢ K ∈ HL ∧ W ∈ H → D ∈ Grp
19 eqid ⊢ Base D = Base D
20 2 3 7 4 19 erngbase ⊢ K ∈ HL ∧ W ∈ H → Base D = TEndo ⁡ K ⁡ W
21 11 20 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H → O ∈ Base D
22 19 8 6 grpid ⊢ D ∈ Grp ∧ O ∈ Base D → O + D O = O ↔ 0 ˙ = O
23 18 21 22 syl2anc ⊢ K ∈ HL ∧ W ∈ H → O + D O = O ↔ 0 ˙ = O
24 15 23 mpbid ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ = O