hdmapip0

Description: Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015)

	Ref	Expression
Hypotheses	hdmapip0.h	$⊢ H = LHyp (K)$
	hdmapip0.u	$⊢ U = DVecH (K) (W)$
	hdmapip0.v	$⊢ V = {Base}_{U}$
	hdmapip0.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmapip0.r	$⊢ R = Scalar (U)$
	hdmapip0.z	$⊢ Z = 0_{R}$
	hdmapip0.s	$⊢ S = HDMap (K) (W)$
	hdmapip0.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapip0.x	$⊢ φ \to X \in V$
Assertion	hdmapip0	$⊢ φ \to (S (X) (X) = Z \leftrightarrow X = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		hdmapip0.h	$⊢ H = LHyp (K)$
2		hdmapip0.u	$⊢ U = DVecH (K) (W)$
3		hdmapip0.v	$⊢ V = {Base}_{U}$
4		hdmapip0.o	$⊢ \underset{˙}{0} = 0_{U}$
5		hdmapip0.r	$⊢ R = Scalar (U)$
6		hdmapip0.z	$⊢ Z = 0_{R}$
7		hdmapip0.s	$⊢ S = HDMap (K) (W)$
8		hdmapip0.k	$⊢ φ \to (K \in HL \land W \in H)$
9		hdmapip0.x	$⊢ φ \to X \in V$
10		eqid	$⊢ ocH (K) (W) = ocH (K) (W)$
11	8	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to (K \in HL \land W \in H)$
12	9	anim1i	$⊢ (φ \land X \neq \underset{˙}{0}) \to (X \in V \land X \neq \underset{˙}{0})$
13		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
14	12 13	sylibr	$⊢ (φ \land X \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
15	1 10 2 3 4 11 14	dochnel	$⊢ (φ \land X \neq \underset{˙}{0}) \to \neg X \in ocH (K) (W) (\{X\})$
16		eqid	$⊢ LFnl (U) = LFnl (U)$
17		eqid	$⊢ LKer (U) = LKer (U)$
18	1 2 8	dvhlmod	$⊢ φ \to U \in LMod$
19		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
20		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
21	1 2 3 19 20 7 8 9	hdmapcl	$⊢ φ \to S (X) \in {Base}_{LCDual (K) (W)}$
22	1 19 20 2 16 8 21	lcdvbaselfl	$⊢ φ \to S (X) \in LFnl (U)$
23	3 5 6 16 17 18 22 9	ellkr2	$⊢ φ \to (X \in LKer (U) (S (X)) \leftrightarrow S (X) (X) = Z)$
24	23	biimpar	$⊢ (φ \land S (X) (X) = Z) \to X \in LKer (U) (S (X))$
25	1 10 2 3 16 17 7 8 9	hdmaplkr	$⊢ φ \to LKer (U) (S (X)) = ocH (K) (W) (\{X\})$
26	25	adantr	$⊢ (φ \land S (X) (X) = Z) \to LKer (U) (S (X)) = ocH (K) (W) (\{X\})$
27	24 26	eleqtrd	$⊢ (φ \land S (X) (X) = Z) \to X \in ocH (K) (W) (\{X\})$
28	27	ex	$⊢ φ \to (S (X) (X) = Z \to X \in ocH (K) (W) (\{X\}))$
29	28	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to (S (X) (X) = Z \to X \in ocH (K) (W) (\{X\}))$
30	15 29	mtod	$⊢ (φ \land X \neq \underset{˙}{0}) \to \neg S (X) (X) = Z$
31	30	neqned	$⊢ (φ \land X \neq \underset{˙}{0}) \to S (X) (X) \neq Z$
32	31	ex	$⊢ φ \to (X \neq \underset{˙}{0} \to S (X) (X) \neq Z)$
33	32	necon4d	$⊢ φ \to (S (X) (X) = Z \to X = \underset{˙}{0})$
34	33	imp	$⊢ (φ \land S (X) (X) = Z) \to X = \underset{˙}{0}$
35		fveq2	$⊢ X = \underset{˙}{0} \to S (X) (X) = S (X) (\underset{˙}{0})$
36	5 6 4 16	lfl0	$⊢ (U \in LMod \land S (X) \in LFnl (U)) \to S (X) (\underset{˙}{0}) = Z$
37	18 22 36	syl2anc	$⊢ φ \to S (X) (\underset{˙}{0}) = Z$
38	35 37	sylan9eqr	$⊢ (φ \land X = \underset{˙}{0}) \to S (X) (X) = Z$
39	34 38	impbida	$⊢ φ \to (S (X) (X) = Z \leftrightarrow X = \underset{˙}{0})$

Metamath Proof Explorer

Theorem hdmapip0

Proof