This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erngbase

Description: The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom W ). TODO: the .t hypothesis isn't used. (Also look at others.) (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses erngset.h ⊢ H = LHyp ⁡ K
erngset.t ⊢ T = LTrn ⁡ K ⁡ W
erngset.e ⊢ E = TEndo ⁡ K ⁡ W
erngset.d ⊢ D = EDRing ⁡ K ⁡ W
erng.c ⊢ C = Base D
Assertion erngbase ⊢ K ∈ V ∧ W ∈ H → C = E

Proof

Step Hyp Ref Expression
1 erngset.h ⊢ H = LHyp ⁡ K
2 erngset.t ⊢ T = LTrn ⁡ K ⁡ W
3 erngset.e ⊢ E = TEndo ⁡ K ⁡ W
4 erngset.d ⊢ D = EDRing ⁡ K ⁡ W
5 erng.c ⊢ C = Base D
6 1 2 3 4 erngset ⊢ K ∈ V ∧ W ∈ H → D = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
7 6 fveq2d ⊢ K ∈ V ∧ W ∈ H → Base D = Base Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
8 3 fvexi ⊢ E ∈ V
9 eqid ⊢ Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
10 9 rngbase ⊢ E ∈ V → E = Base Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
11 8 10 ax-mp ⊢ E = Base Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
12 7 5 11 3eqtr4g ⊢ K ∈ V ∧ W ∈ H → C = E