hgmapval0

Description: Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015)

	Ref	Expression
Hypotheses	hgmapval0.h	$⊢ H = LHyp (K)$
	hgmapval0.u	$⊢ U = DVecH (K) (W)$
	hgmapval0.r	$⊢ R = Scalar (U)$
	hgmapval0.o	$⊢ \underset{˙}{0} = 0_{R}$
	hgmapval0.g	$⊢ G = HGMap (K) (W)$
	hgmapval0.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	hgmapval0	$⊢ φ \to G (\underset{˙}{0}) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		hgmapval0.h	$⊢ H = LHyp (K)$
2		hgmapval0.u	$⊢ U = DVecH (K) (W)$
3		hgmapval0.r	$⊢ R = Scalar (U)$
4		hgmapval0.o	$⊢ \underset{˙}{0} = 0_{R}$
5		hgmapval0.g	$⊢ G = HGMap (K) (W)$
6		hgmapval0.k	$⊢ φ \to (K \in HL \land W \in H)$
7		eqid	$⊢ {Base}_{U} = {Base}_{U}$
8		eqid	$⊢ 0_{U} = 0_{U}$
9	1 2 7 8 6	dvh1dim	$⊢ φ \to \exists x \in {Base}_{U} x \neq 0_{U}$
10		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
11		eqid	$⊢ 0_{LCDual (K) (W)} = 0_{LCDual (K) (W)}$
12		eqid	$⊢ HDMap (K) (W) = HDMap (K) (W)$
13	6	adantr	$⊢ (φ \land x \in {Base}_{U}) \to (K \in HL \land W \in H)$
14		simpr	$⊢ (φ \land x \in {Base}_{U}) \to x \in {Base}_{U}$
15	1 2 7 8 10 11 12 13 14	hdmapeq0	$⊢ (φ \land x \in {Base}_{U}) \to (HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \leftrightarrow x = 0_{U})$
16	15	biimpd	$⊢ (φ \land x \in {Base}_{U}) \to (HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \to x = 0_{U})$
17	16	necon3ad	$⊢ (φ \land x \in {Base}_{U}) \to (x \neq 0_{U} \to \neg HDMap (K) (W) (x) = 0_{LCDual (K) (W)})$
18	17	3impia	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to \neg HDMap (K) (W) (x) = 0_{LCDual (K) (W)}$
19	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
20		eqid	$⊢ \cdot_{U} = \cdot_{U}$
21	7 3 20 4 8	lmod0vs	$⊢ (U \in LMod \land x \in {Base}_{U}) \to \underset{˙}{0} \cdot_{U} x = 0_{U}$
22	19 21	sylan	$⊢ (φ \land x \in {Base}_{U}) \to \underset{˙}{0} \cdot_{U} x = 0_{U}$
23	22	fveq2d	$⊢ (φ \land x \in {Base}_{U}) \to HDMap (K) (W) (\underset{˙}{0} \cdot_{U} x) = HDMap (K) (W) (0_{U})$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25		eqid	$⊢ \cdot_{LCDual (K) (W)} = \cdot_{LCDual (K) (W)}$
26	3 24 4	lmod0cl	$⊢ U \in LMod \to \underset{˙}{0} \in {Base}_{R}$
27	19 26	syl	$⊢ φ \to \underset{˙}{0} \in {Base}_{R}$
28	27	adantr	$⊢ (φ \land x \in {Base}_{U}) \to \underset{˙}{0} \in {Base}_{R}$
29	1 2 7 20 3 24 10 25 12 5 13 14 28	hgmapvs	$⊢ (φ \land x \in {Base}_{U}) \to HDMap (K) (W) (\underset{˙}{0} \cdot_{U} x) = G (\underset{˙}{0}) \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)$
30	1 2 8 10 11 12 6	hdmapval0	$⊢ φ \to HDMap (K) (W) (0_{U}) = 0_{LCDual (K) (W)}$
31	30	adantr	$⊢ (φ \land x \in {Base}_{U}) \to HDMap (K) (W) (0_{U}) = 0_{LCDual (K) (W)}$
32	23 29 31	3eqtr3d	$⊢ (φ \land x \in {Base}_{U}) \to G (\underset{˙}{0}) \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = 0_{LCDual (K) (W)}$
33		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
34		eqid	$⊢ Scalar (LCDual (K) (W)) = Scalar (LCDual (K) (W))$
35		eqid	$⊢ {Base}_{Scalar (LCDual (K) (W))} = {Base}_{Scalar (LCDual (K) (W))}$
36		eqid	$⊢ 0_{Scalar (LCDual (K) (W))} = 0_{Scalar (LCDual (K) (W))}$
37	1 10 6	lcdlvec	$⊢ φ \to LCDual (K) (W) \in LVec$
38	37	adantr	$⊢ (φ \land x \in {Base}_{U}) \to LCDual (K) (W) \in LVec$
39	1 2 13	dvhlmod	$⊢ (φ \land x \in {Base}_{U}) \to U \in LMod$
40	39 26	syl	$⊢ (φ \land x \in {Base}_{U}) \to \underset{˙}{0} \in {Base}_{R}$
41	1 2 3 24 10 34 35 5 13 40	hgmapdcl	$⊢ (φ \land x \in {Base}_{U}) \to G (\underset{˙}{0}) \in {Base}_{Scalar (LCDual (K) (W))}$
42	1 2 7 10 33 12 13 14	hdmapcl	$⊢ (φ \land x \in {Base}_{U}) \to HDMap (K) (W) (x) \in {Base}_{LCDual (K) (W)}$
43	33 25 34 35 36 11 38 41 42	lvecvs0or	$⊢ (φ \land x \in {Base}_{U}) \to (G (\underset{˙}{0}) \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \leftrightarrow (G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))} \lor HDMap (K) (W) (x) = 0_{LCDual (K) (W)}))$
44	32 43	mpbid	$⊢ (φ \land x \in {Base}_{U}) \to (G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))} \lor HDMap (K) (W) (x) = 0_{LCDual (K) (W)})$
45	44	orcomd	$⊢ (φ \land x \in {Base}_{U}) \to (HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \lor G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))})$
46	45	ord	$⊢ (φ \land x \in {Base}_{U}) \to (\neg HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \to G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))})$
47	46	3adant3	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to (\neg HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \to G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))})$
48	18 47	mpd	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))}$
49	48	rexlimdv3a	$⊢ φ \to (\exists x \in {Base}_{U} x \neq 0_{U} \to G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))})$
50	9 49	mpd	$⊢ φ \to G (\underset{˙}{0}) = 0_{Scalar (LCDual (K) (W))}$
51	1 2 3 4 10 34 36 6	lcd0	$⊢ φ \to 0_{Scalar (LCDual (K) (W))} = \underset{˙}{0}$
52	50 51	eqtrd	$⊢ φ \to G (\underset{˙}{0}) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem hgmapval0

Proof