hdmap1l6a

Description: Lemma for hdmap1l6 . Part (6) in Baer p. 47, case 1. (Contributed by NM, 23-Apr-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\})$
	hdmap1l6e.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6e.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1l6e.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	hdmap1l6.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
	hdmap1l6.fg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	hdmap1l6.fe	$⊢ φ \to I (⟨X, F, Z⟩) = E$
Assertion	hdmap1l6a	$⊢ φ \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		hdmap1l6e.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
21		hdmap1l6e.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
22		hdmap1l6e.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
23		hdmap1l6.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
24		hdmap1l6.fg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
25		hdmap1l6.fe	$⊢ φ \to I (⟨X, F, Z⟩) = E$
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	hdmap1l6lem2	$⊢ φ \to M (N (\{Y \underset{˙}{+} Z\})) = L (\{G \underset{˙}{✚} E\})$
27	24 25	oveq12d	$⊢ φ \to I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩) = G \underset{˙}{✚} E$
28	27	sneqd	$⊢ φ \to \{I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)\} = \{G \underset{˙}{✚} E\}$
29	28	fveq2d	$⊢ φ \to L (\{I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)\}) = L (\{G \underset{˙}{✚} E\})$
30	26 29	eqtr4d	$⊢ φ \to M (N (\{Y \underset{˙}{+} Z\})) = L (\{I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)\})$
31	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	hdmap1l6lem1	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) = L (\{F R (G \underset{˙}{✚} E)\})$
32	27	oveq2d	$⊢ φ \to F R (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)) = F R (G \underset{˙}{✚} E)$
33	32	sneqd	$⊢ φ \to \{F R (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))\} = \{F R (G \underset{˙}{✚} E)\}$
34	33	fveq2d	$⊢ φ \to L (\{F R (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))\}) = L (\{F R (G \underset{˙}{✚} E)\})$
35	31 34	eqtr4d	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) = L (\{F R (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))\})$
36	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
37	20	eldifad	$⊢ φ \to Y \in V$
38	21	eldifad	$⊢ φ \to Z \in V$
39	3 4	lmodvacl	$⊢ (U \in LMod \land Y \in V \land Z \in V) \to Y \underset{˙}{+} Z \in V$
40	36 37 38 39	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z \in V$
41	3 4 6 7 36 37 38 23	lmodindp1	$⊢ φ \to Y \underset{˙}{+} Z \neq \underset{˙}{0}$
42		eldifsn	$⊢ Y \underset{˙}{+} Z \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \underset{˙}{+} Z \in V \land Y \underset{˙}{+} Z \neq \underset{˙}{0})$
43	40 41 42	sylanbrc	$⊢ φ \to Y \underset{˙}{+} Z \in (V ∖ \{\underset{˙}{0}\})$
44	1 8 16	lcdlmod	$⊢ φ \to C \in LMod$
45	1 2 16	dvhlvec	$⊢ φ \to U \in LVec$
46	18	eldifad	$⊢ φ \to X \in V$
47	3 6 7 45 37 21 46 23 22	lspindp2	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land \neg Z \in N (\{X, Y\}))$
48	47	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
49	1 2 3 6 7 8 9 13 14 15 16 17 19 48 18 37	hdmap1cl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
50	3 6 7 45 20 38 46 23 22	lspindp1	$⊢ φ \to (N (\{X\}) \neq N (\{Z\}) \land \neg Y \in N (\{X, Z\}))$
51	50	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
52	1 2 3 6 7 8 9 13 14 15 16 17 19 51 18 38	hdmap1cl	$⊢ φ \to I (⟨X, F, Z⟩) \in D$
53	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$
54	44 49 52 53	syl3anc	$⊢ φ \to I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩) \in D$
55		eqid	$⊢ LSubSp (U) = LSubSp (U)$
56	3 55 7 36 37 38	lspprcl	$⊢ φ \to N (\{Y, Z\}) \in LSubSp (U)$
57	3 4 7 36 37 38	lspprvacl	$⊢ φ \to Y \underset{˙}{+} Z \in N (\{Y, Z\})$
58	55 7 36 56 57	ellspsn5	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) \subseteq N (\{Y, Z\})$
59	3 55 7 36 56 46	ellspsn5b	$⊢ φ \to (X \in N (\{Y, Z\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y, Z\}))$
60	22 59	mtbid	$⊢ φ \to \neg N (\{X\}) \subseteq N (\{Y, Z\})$
61		nssne2	$⊢ (N (\{Y \underset{˙}{+} Z\}) \subseteq N (\{Y, Z\}) \land \neg N (\{X\}) \subseteq N (\{Y, Z\})) \to N (\{Y \underset{˙}{+} Z\}) \neq N (\{X\})$
62	58 60 61	syl2anc	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) \neq N (\{X\})$
63	62	necomd	$⊢ φ \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$
64	1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 43 54 63 19	hdmap1eq	$⊢ φ \to (I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩) \leftrightarrow (M (N (\{Y \underset{˙}{+} Z\})) = L (\{I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)\}) \land M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) = L (\{F R (I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩))\})))$
65	30 35 64	mpbir2and	$⊢ φ \to I (⟨X, F, Y \underset{˙}{+} Z⟩) = I (⟨X, F, Y⟩) \underset{˙}{✚} I (⟨X, F, Z⟩)$

Metamath Proof Explorer

Theorem hdmap1l6a

Proof