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

Metamath Proof Explorer

Theorem ldualsbase

Description: Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014)

Ref Expression
Hypotheses ldualsbase.f ⊢ F = Scalar ⁡ W
ldualsbase.l ⊢ L = Base F
ldualsbase.d ⊢ D = LDual ⁡ W
ldualsbase.r ⊢ R = Scalar ⁡ D
ldualsbase.k ⊢ K = Base R
ldualsbase.w ⊢ φ → W ∈ V
Assertion ldualsbase ⊢ φ → K = L

Proof

Step Hyp Ref Expression
1 ldualsbase.f ⊢ F = Scalar ⁡ W
2 ldualsbase.l ⊢ L = Base F
3 ldualsbase.d ⊢ D = LDual ⁡ W
4 ldualsbase.r ⊢ R = Scalar ⁡ D
5 ldualsbase.k ⊢ K = Base R
6 ldualsbase.w ⊢ φ → W ∈ V
7 eqid ⊢ opp r ⁡ F = opp r ⁡ F
8 1 7 3 4 6 ldualsca ⊢ φ → R = opp r ⁡ F
9 8 fveq2d ⊢ φ → Base R = Base opp r ⁡ F
10 7 2 opprbas ⊢ L = Base opp r ⁡ F
11 9 5 10 3eqtr4g ⊢ φ → K = L