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

Metamath Proof Explorer

Theorem ldual0v

Description: The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014)

Ref Expression
Hypotheses ldualv0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ldualv0.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
ldualv0.z ⊢ 0 = ( 0g ‘ 𝑅 )
ldualv0.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualv0.o ⊢ 𝑂 = ( 0g ‘ 𝐷 )
ldualv0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion ldual0v ( 𝜑 → 𝑂 = ( 𝑉 × { 0 } ) )

Proof

Step Hyp Ref Expression
1 ldualv0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ldualv0.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 ldualv0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 ldualv0.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
5 ldualv0.o ⊢ 𝑂 = ( 0g ‘ 𝐷 )
6 ldualv0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 eqid ⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
10 2 3 1 7 lfl0f ⊢ ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
11 6 10 syl ⊢ ( 𝜑 → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
12 7 2 8 4 9 6 11 11 ldualvadd ⊢ ( 𝜑 → ( ( 𝑉 × { 0 } ) ( +g ‘ 𝐷 ) ( 𝑉 × { 0 } ) ) = ( ( 𝑉 × { 0 } ) ∘f ( +g ‘ 𝑅 ) ( 𝑉 × { 0 } ) ) )
13 1 2 8 3 7 6 11 lfladd0l ⊢ ( 𝜑 → ( ( 𝑉 × { 0 } ) ∘f ( +g ‘ 𝑅 ) ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) )
14 12 13 eqtrd ⊢ ( 𝜑 → ( ( 𝑉 × { 0 } ) ( +g ‘ 𝐷 ) ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) )
15 4 6 ldualgrp ⊢ ( 𝜑 → 𝐷 ∈ Grp )
16 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
17 7 4 16 6 11 ldualelvbase ⊢ ( 𝜑 → ( 𝑉 × { 0 } ) ∈ ( Base ‘ 𝐷 ) )
18 16 9 5 grpid ⊢ ( ( 𝐷 ∈ Grp ∧ ( 𝑉 × { 0 } ) ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑉 × { 0 } ) ( +g ‘ 𝐷 ) ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) ↔ 𝑂 = ( 𝑉 × { 0 } ) ) )
19 15 17 18 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑉 × { 0 } ) ( +g ‘ 𝐷 ) ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) ↔ 𝑂 = ( 𝑉 × { 0 } ) ) )
20 14 19 mpbid ⊢ ( 𝜑 → 𝑂 = ( 𝑉 × { 0 } ) )