hgmapval1

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

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

Proof

Step	Hyp	Ref	Expression
1		hgmapval1.h	$⊢ H = LHyp (K)$
2		hgmapval1.u	$⊢ U = DVecH (K) (W)$
3		hgmapval1.r	$⊢ R = Scalar (U)$
4		hgmapval1.i	$⊢ \underset{˙}{1} = 1_{R}$
5		hgmapval1.g	$⊢ G = HGMap (K) (W)$
6		hgmapval1.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	$⊢ Scalar (LCDual (K) (W)) = Scalar (LCDual (K) (W))$
12		eqid	$⊢ 1_{Scalar (LCDual (K) (W))} = 1_{Scalar (LCDual (K) (W))}$
13	1 2 3 4 10 11 12 6	lcd1	$⊢ φ \to 1_{Scalar (LCDual (K) (W))} = \underset{˙}{1}$
14	13	oveq1d	$⊢ φ \to 1_{Scalar (LCDual (K) (W))} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = \underset{˙}{1} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)$
15	14	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to 1_{Scalar (LCDual (K) (W))} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = \underset{˙}{1} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)$
16	1 10 6	lcdlmod	$⊢ φ \to LCDual (K) (W) \in LMod$
17	16	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to LCDual (K) (W) \in LMod$
18		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
19		eqid	$⊢ HDMap (K) (W) = HDMap (K) (W)$
20	6	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to (K \in HL \land W \in H)$
21		simp2	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to x \in {Base}_{U}$
22	1 2 7 10 18 19 20 21	hdmapcl	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to HDMap (K) (W) (x) \in {Base}_{LCDual (K) (W)}$
23		eqid	$⊢ \cdot_{LCDual (K) (W)} = \cdot_{LCDual (K) (W)}$
24	18 11 23 12	lmodvs1	$⊢ (LCDual (K) (W) \in LMod \land HDMap (K) (W) (x) \in {Base}_{LCDual (K) (W)}) \to 1_{Scalar (LCDual (K) (W))} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = HDMap (K) (W) (x)$
25	17 22 24	syl2anc	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to 1_{Scalar (LCDual (K) (W))} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = HDMap (K) (W) (x)$
26	15 25	eqtr3d	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to \underset{˙}{1} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = HDMap (K) (W) (x)$
27	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
28	27	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to U \in LMod$
29		eqid	$⊢ \cdot_{U} = \cdot_{U}$
30	7 3 29 4	lmodvs1	$⊢ (U \in LMod \land x \in {Base}_{U}) \to \underset{˙}{1} \cdot_{U} x = x$
31	28 21 30	syl2anc	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to \underset{˙}{1} \cdot_{U} x = x$
32	31	fveq2d	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to HDMap (K) (W) (\underset{˙}{1} \cdot_{U} x) = HDMap (K) (W) (x)$
33		eqid	$⊢ {Base}_{R} = {Base}_{R}$
34	3	lmodring	$⊢ U \in LMod \to R \in Ring$
35	33 4	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
36	27 34 35	3syl	$⊢ φ \to \underset{˙}{1} \in {Base}_{R}$
37	36	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to \underset{˙}{1} \in {Base}_{R}$
38	1 2 7 29 3 33 10 23 19 5 20 21 37	hgmapvs	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to HDMap (K) (W) (\underset{˙}{1} \cdot_{U} x) = G (\underset{˙}{1}) \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)$
39	26 32 38	3eqtr2rd	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to G (\underset{˙}{1}) \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = \underset{˙}{1} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)$
40		eqid	$⊢ {Base}_{Scalar (LCDual (K) (W))} = {Base}_{Scalar (LCDual (K) (W))}$
41		eqid	$⊢ 0_{LCDual (K) (W)} = 0_{LCDual (K) (W)}$
42	1 10 6	lcdlvec	$⊢ φ \to LCDual (K) (W) \in LVec$
43	42	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to LCDual (K) (W) \in LVec$
44	1 2 3 33 5 6 36	hgmapcl	$⊢ φ \to G (\underset{˙}{1}) \in {Base}_{R}$
45	1 2 3 33 10 11 40 6	lcdsbase	$⊢ φ \to {Base}_{Scalar (LCDual (K) (W))} = {Base}_{R}$
46	44 45	eleqtrrd	$⊢ φ \to G (\underset{˙}{1}) \in {Base}_{Scalar (LCDual (K) (W))}$
47	46	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to G (\underset{˙}{1}) \in {Base}_{Scalar (LCDual (K) (W))}$
48	36 45	eleqtrrd	$⊢ φ \to \underset{˙}{1} \in {Base}_{Scalar (LCDual (K) (W))}$
49	48	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to \underset{˙}{1} \in {Base}_{Scalar (LCDual (K) (W))}$
50		simp3	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to x \neq 0_{U}$
51	1 2 7 8 10 41 19 20 21	hdmapeq0	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to (HDMap (K) (W) (x) = 0_{LCDual (K) (W)} \leftrightarrow x = 0_{U})$
52	51	necon3bid	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to (HDMap (K) (W) (x) \neq 0_{LCDual (K) (W)} \leftrightarrow x \neq 0_{U})$
53	50 52	mpbird	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to HDMap (K) (W) (x) \neq 0_{LCDual (K) (W)}$
54	18 23 11 40 41 43 47 49 22 53	lvecvscan2	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to (G (\underset{˙}{1}) \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) = \underset{˙}{1} \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) \leftrightarrow G (\underset{˙}{1}) = \underset{˙}{1})$
55	39 54	mpbid	$⊢ (φ \land x \in {Base}_{U} \land x \neq 0_{U}) \to G (\underset{˙}{1}) = \underset{˙}{1}$
56	55	rexlimdv3a	$⊢ φ \to (\exists x \in {Base}_{U} x \neq 0_{U} \to G (\underset{˙}{1}) = \underset{˙}{1})$
57	9 56	mpd	$⊢ φ \to G (\underset{˙}{1}) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem hgmapval1

Proof