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 } ) )