hgmap11

Description: The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015)

	Ref	Expression
Hypotheses	hgmap11.h	$⊢ H = LHyp (K)$
	hgmap11.u	$⊢ U = DVecH (K) (W)$
	hgmap11.r	$⊢ R = Scalar (U)$
	hgmap11.b	$⊢ B = {Base}_{R}$
	hgmap11.g	$⊢ G = HGMap (K) (W)$
	hgmap11.k	$⊢ φ \to (K \in HL \land W \in H)$
	hgmap11.x	$⊢ φ \to X \in B$
	hgmap11.y	$⊢ φ \to Y \in B$
Assertion	hgmap11	$⊢ φ \to (G (X) = G (Y) \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		hgmap11.h	$⊢ H = LHyp (K)$
2		hgmap11.u	$⊢ U = DVecH (K) (W)$
3		hgmap11.r	$⊢ R = Scalar (U)$
4		hgmap11.b	$⊢ B = {Base}_{R}$
5		hgmap11.g	$⊢ G = HGMap (K) (W)$
6		hgmap11.k	$⊢ φ \to (K \in HL \land W \in H)$
7		hgmap11.x	$⊢ φ \to X \in B$
8		hgmap11.y	$⊢ φ \to Y \in B$
9		eqid	$⊢ {Base}_{U} = {Base}_{U}$
10		eqid	$⊢ 0_{U} = 0_{U}$
11	1 2 9 10 6	dvh1dim	$⊢ φ \to \exists t \in {Base}_{U} t \neq 0_{U}$
12	11	adantr	$⊢ (φ \land G (X) = G (Y)) \to \exists t \in {Base}_{U} t \neq 0_{U}$
13		simp1r	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X) = G (Y)$
14	13	oveq1d	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t) = G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
15		eqid	$⊢ \cdot_{U} = \cdot_{U}$
16		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
17		eqid	$⊢ \cdot_{LCDual (K) (W)} = \cdot_{LCDual (K) (W)}$
18		eqid	$⊢ HDMap (K) (W) = HDMap (K) (W)$
19		simp1l	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to φ$
20	19 6	syl	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to (K \in HL \land W \in H)$
21		simp2	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to t \in {Base}_{U}$
22	19 7	syl	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to X \in B$
23	1 2 9 15 3 4 16 17 18 5 20 21 22	hgmapvs	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (X \cdot_{U} t) = G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
24	19 8	syl	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to Y \in B$
25	1 2 9 15 3 4 16 17 18 5 20 21 24	hgmapvs	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (Y \cdot_{U} t) = G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
26	14 23 25	3eqtr4d	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (X \cdot_{U} t) = HDMap (K) (W) (Y \cdot_{U} t)$
27	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
28	19 27	syl	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to U \in LMod$
29	9 3 15 4	lmodvscl	$⊢ (U \in LMod \land X \in B \land t \in {Base}_{U}) \to X \cdot_{U} t \in {Base}_{U}$
30	28 22 21 29	syl3anc	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to X \cdot_{U} t \in {Base}_{U}$
31	9 3 15 4	lmodvscl	$⊢ (U \in LMod \land Y \in B \land t \in {Base}_{U}) \to Y \cdot_{U} t \in {Base}_{U}$
32	28 24 21 31	syl3anc	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to Y \cdot_{U} t \in {Base}_{U}$
33	1 2 9 18 20 30 32	hdmap11	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to (HDMap (K) (W) (X \cdot_{U} t) = HDMap (K) (W) (Y \cdot_{U} t) \leftrightarrow X \cdot_{U} t = Y \cdot_{U} t)$
34	26 33	mpbid	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to X \cdot_{U} t = Y \cdot_{U} t$
35	1 2 6	dvhlvec	$⊢ φ \to U \in LVec$
36	19 35	syl	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to U \in LVec$
37		simp3	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to t \neq 0_{U}$
38	9 15 3 4 10 36 22 24 21 37	lvecvscan2	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to (X \cdot_{U} t = Y \cdot_{U} t \leftrightarrow X = Y)$
39	34 38	mpbid	$⊢ ((φ \land G (X) = G (Y)) \land t \in {Base}_{U} \land t \neq 0_{U}) \to X = Y$
40	39	rexlimdv3a	$⊢ (φ \land G (X) = G (Y)) \to (\exists t \in {Base}_{U} t \neq 0_{U} \to X = Y)$
41	12 40	mpd	$⊢ (φ \land G (X) = G (Y)) \to X = Y$
42	41	ex	$⊢ φ \to (G (X) = G (Y) \to X = Y)$
43		fveq2	$⊢ X = Y \to G (X) = G (Y)$
44	42 43	impbid1	$⊢ φ \to (G (X) = G (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem hgmap11

Proof