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

Metamath Proof Explorer

Theorem erngbase-rN

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 ). (Contributed by NM, 9-Jun-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 erngset.h-r ⊢ H = LHyp ⁡ K
2 erngset.t-r ⊢ T = LTrn ⁡ K ⁡ W
3 erngset.e-r ⊢ E = TEndo ⁡ K ⁡ W
4 erngset.d-r ⊢ D = EDRing R ⁡ K ⁡ W
5 erng.c-r ⊢ C = Base D
6 1 2 3 4 erngset-rN ⊢ K ∈ V ∧ W ∈ H → D = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ t ∘ s
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 ⟼ t ∘ s
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 ⟼ t ∘ s = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ t ∘ s
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 ⟼ t ∘ s
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 ⟼ t ∘ s
12 7 5 11 3eqtr4g ⊢ K ∈ V ∧ W ∈ H → C = E