hdmap1l6h

Description: Lemmma for hdmap1l6 . Part (6) of Baer p. 48 line 2. (Contributed by NM, 1-May-2015)

	Ref	Expression
Hypotheses	hdmap1l6.h	$⊢ H = LHyp (K)$
	hdmap1l6.u	$⊢ U = DVecH (K) (W)$
	hdmap1l6.v	$⊢ V = {Base}_{U}$
	hdmap1l6.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmap1l6.s	$⊢ \underset{˙}{-} = -_{U}$
	hdmap1l6c.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap1l6.n	$⊢ N = LSpan (U)$
	hdmap1l6.c	$⊢ C = LCDual (K) (W)$
	hdmap1l6.d	$⊢ D = {Base}_{C}$
	hdmap1l6.a	$⊢ \underset{˙}{✚} = +_{C}$
	hdmap1l6.r	$⊢ R = -_{C}$
	hdmap1l6.q	$⊢ Q = 0_{C}$
	hdmap1l6.l	$⊢ L = LSpan (C)$
	hdmap1l6.m	$⊢ M = mapd (K) (W)$
	hdmap1l6.i	$⊢ I = HDMap1 (K) (W)$
	hdmap1l6.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap1l6.f	$⊢ φ \to F \in D$
	hdmap1l6cl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6.mn	$⊢ φ \to M (N (\{X\})) = L (\{F\})$
	hdmap1l6d.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	hdmap1l6d.yz	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
	hdmap1l6d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6d.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6d.w	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6d.wn	$⊢ φ \to \neg w \in N (\{X, Y\})$
Assertion	hdmap1l6h	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Proof

Step	Hyp	Ref	Expression
1		hdmap1l6.h	$⊢ H = LHyp (K)$
2		hdmap1l6.u	$⊢ U = DVecH (K) (W)$
3		hdmap1l6.v	$⊢ V = {Base}_{U}$
4		hdmap1l6.p	$⊢ \underset{˙}{+} = +_{U}$
5		hdmap1l6.s	$⊢ \underset{˙}{-} = -_{U}$
6		hdmap1l6c.o	$⊢ \underset{˙}{0} = 0_{U}$
7		hdmap1l6.n	$⊢ N = LSpan (U)$
8		hdmap1l6.c	$⊢ C = LCDual (K) (W)$
9		hdmap1l6.d	$⊢ D = {Base}_{C}$
10		hdmap1l6.a	$⊢ \underset{˙}{✚} = +_{C}$
11		hdmap1l6.r	$⊢ R = -_{C}$
12		hdmap1l6.q	$⊢ Q = 0_{C}$
13		hdmap1l6.l	$⊢ L = LSpan (C)$
14		hdmap1l6.m	$⊢ M = mapd (K) (W)$
15		hdmap1l6.i	$⊢ I = HDMap1 (K) (W)$
16		hdmap1l6.k	$⊢ φ \to (K \in HL \land W \in H)$
17		hdmap1l6.f	$⊢ φ \to F \in D$
18		hdmap1l6cl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
19		hdmap1l6.mn	$⊢ φ \to M (N (\{X\})) = L (\{F\})$
20		hdmap1l6d.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
21		hdmap1l6d.yz	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
22		hdmap1l6d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
23		hdmap1l6d.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
24		hdmap1l6d.w	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
25		hdmap1l6d.wn	$⊢ φ \to \neg w \in N (\{X, Y\})$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	hdmap1l6g	$⊢ φ \to I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩) = (I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y⟩)) \underset{˙}{✚} I (⟨X, F, Z⟩)$
27	1 8 16	lcdlmod	$⊢ φ \to C \in LMod$
28	1 2 16	dvhlvec	$⊢ φ \to U \in LVec$
29	24	eldifad	$⊢ φ \to w \in V$
30	18	eldifad	$⊢ φ \to X \in V$
31	22	eldifad	$⊢ φ \to Y \in V$
32	3 7 28 29 30 31 25	lspindpi	$⊢ φ \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{Y\}))$
33	32	simpld	$⊢ φ \to N (\{w\}) \neq N (\{X\})$
34	33	necomd	$⊢ φ \to N (\{X\}) \neq N (\{w\})$
35	1 2 3 6 7 8 9 13 14 15 16 17 19 34 18 29	hdmap1cl	$⊢ φ \to I (⟨X, F, w⟩) \in D$
36	23	eldifad	$⊢ φ \to Z \in V$
37	3 7 28 30 31 36 20	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$
38	37	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
39	1 2 3 6 7 8 9 13 14 15 16 17 19 38 18 31	hdmap1cl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
40	37	simprd	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
41	1 2 3 6 7 8 9 13 14 15 16 17 19 40 18 36	hdmap1cl	$⊢ φ \to I (⟨X, F, Z⟩) \in D$
42	9 10	lmodass	$⊢ (C \in LMod \land (I (⟨X, F, w⟩) \in D \land I (⟨X, F, Y⟩) \in D \land I (⟨X, F, Z⟩) \in D)) \to (I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y⟩)) \underset{˙}{✚} I (⟨X, F, Z⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))$
43	27 35 39 41 42	syl13anc	$⊢ φ \to (I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y⟩)) \underset{˙}{✚} I (⟨X, F, Z⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))$
44	26 43	eqtrd	$⊢ φ \to I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))$
45	3 4 6 7 28 18 22 23 24 21 38 25	mapdindp1	$⊢ φ \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$
46	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
47	3 4	lmodvacl	$⊢ (U \in LMod \land Y \in V \land Z \in V) \to Y \underset{˙}{+} Z \in V$
48	46 31 36 47	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z \in V$
49	1 2 3 6 7 8 9 13 14 15 16 17 19 45 18 48	hdmap1cl	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) \in D$
50	9 10	lmodvacl	$⊢ (C \in LMod \land I (⟨X, F, Y⟩) \in D \land I (⟨X, F, Z⟩) \in D) \to I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩) \in D$
51	27 39 41 50	syl3anc	$⊢ φ \to I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩) \in D$
52	9 10	lmodlcan	$⊢ (C \in LMod \land (I (⟨X, F, Y \underset{˙}{+} Z⟩) \in D \land I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩) \in D \land I (⟨X, F, w⟩) \in D)) \to (I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)) \leftrightarrow I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))$
53	27 49 51 35 52	syl13anc	$⊢ φ \to (I (⟨X, F, w⟩) \underset{˙}{✚} I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, w⟩) \underset{˙}{✚} (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)) \leftrightarrow I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))$
54	44 53	mpbid	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Metamath Proof Explorer

Theorem hdmap1l6h

Proof