hdmap11

Description: Part of proof of part 12 in Baer p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015)

	Ref	Expression
Hypotheses	hdmap12d.h	$⊢ H = LHyp (K)$
	hdmap12d.u	$⊢ U = DVecH (K) (W)$
	hdmap12d.v	$⊢ V = {Base}_{U}$
	hdmap12d.s	$⊢ S = HDMap (K) (W)$
	hdmap12d.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap12d.x	$⊢ φ \to X \in V$
	hdmap12d.y	$⊢ φ \to Y \in V$
Assertion	hdmap11	$⊢ φ \to (S (X) = S (Y) \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		hdmap12d.h	$⊢ H = LHyp (K)$
2		hdmap12d.u	$⊢ U = DVecH (K) (W)$
3		hdmap12d.v	$⊢ V = {Base}_{U}$
4		hdmap12d.s	$⊢ S = HDMap (K) (W)$
5		hdmap12d.k	$⊢ φ \to (K \in HL \land W \in H)$
6		hdmap12d.x	$⊢ φ \to X \in V$
7		hdmap12d.y	$⊢ φ \to Y \in V$
8		eqid	$⊢ -_{U} = -_{U}$
9		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
10		eqid	$⊢ -_{LCDual (K) (W)} = -_{LCDual (K) (W)}$
11	1 2 3 8 9 10 4 5 6 7	hdmapsub	$⊢ φ \to S (X -_{U} Y) = S (X) -_{LCDual (K) (W)} S (Y)$
12	11	eqeq1d	$⊢ φ \to (S (X -_{U} Y) = 0_{LCDual (K) (W)} \leftrightarrow S (X) -_{LCDual (K) (W)} S (Y) = 0_{LCDual (K) (W)})$
13		eqid	$⊢ 0_{U} = 0_{U}$
14		eqid	$⊢ 0_{LCDual (K) (W)} = 0_{LCDual (K) (W)}$
15	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
16	3 8	lmodvsubcl	$⊢ (U \in LMod \land X \in V \land Y \in V) \to X -_{U} Y \in V$
17	15 6 7 16	syl3anc	$⊢ φ \to X -_{U} Y \in V$
18	1 2 3 13 9 14 4 5 17	hdmapeq0	$⊢ φ \to (S (X -_{U} Y) = 0_{LCDual (K) (W)} \leftrightarrow X -_{U} Y = 0_{U})$
19	1 9 5	lcdlmod	$⊢ φ \to LCDual (K) (W) \in LMod$
20		lmodgrp	$⊢ LCDual (K) (W) \in LMod \to LCDual (K) (W) \in Grp$
21	19 20	syl	$⊢ φ \to LCDual (K) (W) \in Grp$
22		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
23	1 2 3 9 22 4 5 6	hdmapcl	$⊢ φ \to S (X) \in {Base}_{LCDual (K) (W)}$
24	1 2 3 9 22 4 5 7	hdmapcl	$⊢ φ \to S (Y) \in {Base}_{LCDual (K) (W)}$
25	22 14 10	grpsubeq0	$⊢ (LCDual (K) (W) \in Grp \land S (X) \in {Base}_{LCDual (K) (W)} \land S (Y) \in {Base}_{LCDual (K) (W)}) \to (S (X) -_{LCDual (K) (W)} S (Y) = 0_{LCDual (K) (W)} \leftrightarrow S (X) = S (Y))$
26	21 23 24 25	syl3anc	$⊢ φ \to (S (X) -_{LCDual (K) (W)} S (Y) = 0_{LCDual (K) (W)} \leftrightarrow S (X) = S (Y))$
27	12 18 26	3bitr3rd	$⊢ φ \to (S (X) = S (Y) \leftrightarrow X -_{U} Y = 0_{U})$
28		lmodgrp	$⊢ U \in LMod \to U \in Grp$
29	15 28	syl	$⊢ φ \to U \in Grp$
30	3 13 8	grpsubeq0	$⊢ (U \in Grp \land X \in V \land Y \in V) \to (X -_{U} Y = 0_{U} \leftrightarrow X = Y)$
31	29 6 7 30	syl3anc	$⊢ φ \to (X -_{U} Y = 0_{U} \leftrightarrow X = Y)$
32	27 31	bitrd	$⊢ φ \to (S (X) = S (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem hdmap11

Proof