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

Metamath Proof Explorer

Theorem dvhsca

Description: The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014)

Ref Expression
Hypotheses dvhsca.h ⊢ H = LHyp ⁡ K
dvhsca.d ⊢ D = EDRing ⁡ K ⁡ W
dvhsca.u ⊢ U = DVecH ⁡ K ⁡ W
dvhsca.f ⊢ F = Scalar ⁡ U
Assertion dvhsca ⊢ K ∈ X ∧ W ∈ H → F = D

Proof

Step Hyp Ref Expression
1 dvhsca.h ⊢ H = LHyp ⁡ K
2 dvhsca.d ⊢ D = EDRing ⁡ K ⁡ W
3 dvhsca.u ⊢ U = DVecH ⁡ K ⁡ W
4 dvhsca.f ⊢ F = Scalar ⁡ U
5 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
6 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
7 1 5 6 2 3 dvhset ⊢ K ∈ X ∧ W ∈ H → U = Base ndx LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W + ndx f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W , g ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ 1 st ⁡ f ∘ 1 st ⁡ g h ∈ LTrn ⁡ K ⁡ W ⟼ 2 nd ⁡ f ⁡ h ∘ 2 nd ⁡ g ⁡ h Scalar ⁡ ndx D ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ s ⁡ 1 st ⁡ f s ∘ 2 nd ⁡ f
8 7 fveq2d ⊢ K ∈ X ∧ W ∈ H → Scalar ⁡ U = Scalar ⁡ Base ndx LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W + ndx f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W , g ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ 1 st ⁡ f ∘ 1 st ⁡ g h ∈ LTrn ⁡ K ⁡ W ⟼ 2 nd ⁡ f ⁡ h ∘ 2 nd ⁡ g ⁡ h Scalar ⁡ ndx D ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ s ⁡ 1 st ⁡ f s ∘ 2 nd ⁡ f
9 2 fvexi ⊢ D ∈ V
10 eqid ⊢ Base ndx LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W + ndx f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W , g ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ 1 st ⁡ f ∘ 1 st ⁡ g h ∈ LTrn ⁡ K ⁡ W ⟼ 2 nd ⁡ f ⁡ h ∘ 2 nd ⁡ g ⁡ h Scalar ⁡ ndx D ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ s ⁡ 1 st ⁡ f s ∘ 2 nd ⁡ f = Base ndx LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W + ndx f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W , g ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ 1 st ⁡ f ∘ 1 st ⁡ g h ∈ LTrn ⁡ K ⁡ W ⟼ 2 nd ⁡ f ⁡ h ∘ 2 nd ⁡ g ⁡ h Scalar ⁡ ndx D ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ s ⁡ 1 st ⁡ f s ∘ 2 nd ⁡ f
11 10 lmodsca ⊢ D ∈ V → D = Scalar ⁡ Base ndx LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W + ndx f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W , g ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ 1 st ⁡ f ∘ 1 st ⁡ g h ∈ LTrn ⁡ K ⁡ W ⟼ 2 nd ⁡ f ⁡ h ∘ 2 nd ⁡ g ⁡ h Scalar ⁡ ndx D ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ s ⁡ 1 st ⁡ f s ∘ 2 nd ⁡ f
12 9 11 ax-mp ⊢ D = Scalar ⁡ Base ndx LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W + ndx f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W , g ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ 1 st ⁡ f ∘ 1 st ⁡ g h ∈ LTrn ⁡ K ⁡ W ⟼ 2 nd ⁡ f ⁡ h ∘ 2 nd ⁡ g ⁡ h Scalar ⁡ ndx D ∪ ⋅ ndx s ∈ TEndo ⁡ K ⁡ W , f ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ⟼ s ⁡ 1 st ⁡ f s ∘ 2 nd ⁡ f
13 8 4 12 3eqtr4g ⊢ K ∈ X ∧ W ∈ H → F = D