ldual0v

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

	Ref	Expression
Hypotheses	ldualv0.v	$⊢ V = {Base}_{W}$
	ldualv0.r	$⊢ R = Scalar (W)$
	ldualv0.z	$⊢ \underset{˙}{0} = 0_{R}$
	ldualv0.d	$⊢ D = LDual (W)$
	ldualv0.o	$⊢ O = 0_{D}$
	ldualv0.w	$⊢ φ \to W \in LMod$
Assertion	ldual0v	$⊢ φ \to O = V \times \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		ldualv0.v	$⊢ V = {Base}_{W}$
2		ldualv0.r	$⊢ R = Scalar (W)$
3		ldualv0.z	$⊢ \underset{˙}{0} = 0_{R}$
4		ldualv0.d	$⊢ D = LDual (W)$
5		ldualv0.o	$⊢ O = 0_{D}$
6		ldualv0.w	$⊢ φ \to W \in LMod$
7		eqid	$⊢ LFnl (W) = LFnl (W)$
8		eqid	$⊢ +_{R} = +_{R}$
9		eqid	$⊢ +_{D} = +_{D}$
10	2 3 1 7	lfl0f	$⊢ W \in LMod \to V \times \{\underset{˙}{0}\} \in LFnl (W)$
11	6 10	syl	$⊢ φ \to V \times \{\underset{˙}{0}\} \in LFnl (W)$
12	7 2 8 4 9 6 11 11	ldualvadd	$⊢ φ \to (V \times \{\underset{˙}{0}\}) +_{D} (V \times \{\underset{˙}{0}\}) = (V \times \{\underset{˙}{0}\}) {+_{R}}_{f} (V \times \{\underset{˙}{0}\})$
13	1 2 8 3 7 6 11	lfladd0l	$⊢ φ \to (V \times \{\underset{˙}{0}\}) {+_{R}}_{f} (V \times \{\underset{˙}{0}\}) = V \times \{\underset{˙}{0}\}$
14	12 13	eqtrd	$⊢ φ \to (V \times \{\underset{˙}{0}\}) +_{D} (V \times \{\underset{˙}{0}\}) = V \times \{\underset{˙}{0}\}$
15	4 6	ldualgrp	$⊢ φ \to D \in Grp$
16		eqid	$⊢ {Base}_{D} = {Base}_{D}$
17	7 4 16 6 11	ldualelvbase	$⊢ φ \to V \times \{\underset{˙}{0}\} \in {Base}_{D}$
18	16 9 5	grpid	$⊢ (D \in Grp \land V \times \{\underset{˙}{0}\} \in {Base}_{D}) \to ((V \times \{\underset{˙}{0}\}) +_{D} (V \times \{\underset{˙}{0}\}) = V \times \{\underset{˙}{0}\} \leftrightarrow O = V \times \{\underset{˙}{0}\})$
19	15 17 18	syl2anc	$⊢ φ \to ((V \times \{\underset{˙}{0}\}) +_{D} (V \times \{\underset{˙}{0}\}) = V \times \{\underset{˙}{0}\} \leftrightarrow O = V \times \{\underset{˙}{0}\})$
20	14 19	mpbid	$⊢ φ \to O = V \times \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem ldual0v

Proof