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

Metamath Proof Explorer

Theorem ldual0

Description: The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014)

Ref Expression
Hypotheses ldual0.r ⊢ R = Scalar ⁡ W
ldual0.z ⊢ 0 ˙ = 0 R
ldual0.d ⊢ D = LDual ⁡ W
ldual0.s ⊢ S = Scalar ⁡ D
ldual0.o ⊢ O = 0 S
ldual0.w ⊢ φ → W ∈ LMod
Assertion ldual0 ⊢ φ → O = 0 ˙

Proof

Step Hyp Ref Expression
1 ldual0.r ⊢ R = Scalar ⁡ W
2 ldual0.z ⊢ 0 ˙ = 0 R
3 ldual0.d ⊢ D = LDual ⁡ W
4 ldual0.s ⊢ S = Scalar ⁡ D
5 ldual0.o ⊢ O = 0 S
6 ldual0.w ⊢ φ → W ∈ LMod
7 eqid ⊢ opp r ⁡ R = opp r ⁡ R
8 1 7 3 4 6 ldualsca ⊢ φ → S = opp r ⁡ R
9 8 fveq2d ⊢ φ → 0 S = 0 opp r ⁡ R
10 7 2 oppr0 ⊢ 0 ˙ = 0 opp r ⁡ R
11 9 5 10 3eqtr4g ⊢ φ → O = 0 ˙