Metamath Proof Explorer

Theorem erngset

Description: The division ring on trace-preserving endomorphisms for a fiducial co-atom W . (Contributed by NM, 5-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
Assertion 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

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 1 erngfset ⊢ K ∈ V → EDRing ⁡ K = w ∈ H ⟼ Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
6 5 fveq1d ⊢ K ∈ V → EDRing ⁡ K ⁡ W = w ∈ H ⟼ Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t ⁡ W
7 4 6 syl5eq ⊢ K ∈ V → D = w ∈ H ⟼ Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t ⁡ W
8 fveq2 ⊢ w = W → TEndo ⁡ K ⁡ w = TEndo ⁡ K ⁡ W
9 8 opeq2d ⊢ w = W → Base ndx TEndo ⁡ K ⁡ w = Base ndx TEndo ⁡ K ⁡ W
10 tpeq1 ⊢ Base ndx TEndo ⁡ K ⁡ w = Base ndx TEndo ⁡ K ⁡ W → Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx TEndo ⁡ K ⁡ W + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
11 3 opeq2i ⊢ Base ndx E = Base ndx TEndo ⁡ K ⁡ W
12 tpeq1 ⊢ Base ndx E = Base ndx TEndo ⁡ K ⁡ W → Base ndx E + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx TEndo ⁡ K ⁡ W + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
13 11 12 ax-mp ⊢ Base ndx E + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx TEndo ⁡ K ⁡ W + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
14 10 13 eqtr4di ⊢ Base ndx TEndo ⁡ K ⁡ w = Base ndx TEndo ⁡ K ⁡ W → Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx E + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
15 9 14 syl ⊢ w = W → Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx E + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
16 8 3 eqtr4di ⊢ w = W → TEndo ⁡ K ⁡ w = E
17 fveq2 ⊢ w = W → LTrn ⁡ K ⁡ w = LTrn ⁡ K ⁡ W
18 17 2 eqtr4di ⊢ w = W → LTrn ⁡ K ⁡ w = T
19 eqidd ⊢ w = W → s ⁡ f ∘ t ⁡ f = s ⁡ f ∘ t ⁡ f
20 18 19 mpteq12dv ⊢ w = W → f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f = f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
21 16 16 20 mpoeq123dv ⊢ w = W → s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
22 21 opeq2d ⊢ w = W → + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f = + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
23 22 tpeq2d ⊢ w = W → Base ndx E + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
24 eqidd ⊢ w = W → s ∘ t = s ∘ t
25 16 16 24 mpoeq123dv ⊢ w = W → s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = s ∈ E , t ∈ E ⟼ s ∘ t
26 25 opeq2d ⊢ w = W → ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
27 26 tpeq3d ⊢ w = W → Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
28 15 23 27 3eqtrd ⊢ w = W → Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
29 eqid ⊢ w ∈ H ⟼ Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t = w ∈ H ⟼ Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t
30 tpex ⊢ Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t ∈ V
31 28 29 30 fvmpt ⊢ W ∈ H → w ∈ H ⟼ Base ndx TEndo ⁡ K ⁡ w + ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ f ∈ LTrn ⁡ K ⁡ w ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ TEndo ⁡ K ⁡ w , t ∈ TEndo ⁡ K ⁡ w ⟼ s ∘ t ⁡ W = Base ndx E + ndx s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f ⋅ ndx s ∈ E , t ∈ E ⟼ s ∘ t
32 7 31 sylan9eq ⊢ 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