hdmap1l6lem2

Description: Lemma for hdmap1l6 . Part (6) in Baer p. 47, lines 20-22. (Contributed by NM, 13-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	hdmap1l6lem2	$⊢ φ \to M (N (\{Y \underset{˙}{+} Z\})) = L (\{G \underset{˙}{✚} E\})$

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		eqid	$⊢ LSubSp (U) = LSubSp (U)$
27	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
28	20	eldifad	$⊢ φ \to Y \in V$
29	3 26 7	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
30	27 28 29	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
31	21	eldifad	$⊢ φ \to Z \in V$
32	3 26 7	lspsncl	$⊢ (U \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (U)$
33	27 31 32	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (U)$
34		eqid	$⊢ LSSum (U) = LSSum (U)$
35	26 34	lsmcl	$⊢ (U \in LMod \land N (\{Y\}) \in LSubSp (U) \land N (\{Z\}) \in LSubSp (U)) \to N (\{Y\}) LSSum (U) N (\{Z\}) \in LSubSp (U)$
36	27 30 33 35	syl3anc	$⊢ φ \to N (\{Y\}) LSSum (U) N (\{Z\}) \in LSubSp (U)$
37	18	eldifad	$⊢ φ \to X \in V$
38	3 4	lmodvacl	$⊢ (U \in LMod \land Y \in V \land Z \in V) \to Y \underset{˙}{+} Z \in V$
39	27 28 31 38	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z \in V$
40	3 5	lmodvsubcl	$⊢ (U \in LMod \land X \in V \land Y \underset{˙}{+} Z \in V) \to X \underset{˙}{-} (Y \underset{˙}{+} Z) \in V$
41	27 37 39 40	syl3anc	$⊢ φ \to X \underset{˙}{-} (Y \underset{˙}{+} Z) \in V$
42	3 26 7	lspsncl	$⊢ (U \in LMod \land X \underset{˙}{-} (Y \underset{˙}{+} Z) \in V) \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) \in LSubSp (U)$
43	27 41 42	syl2anc	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) \in LSubSp (U)$
44	3 26 7	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
45	27 37 44	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
46	26 34	lsmcl	$⊢ (U \in LMod \land N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) \in LSubSp (U) \land N (\{X\}) \in LSubSp (U)) \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\}) \in LSubSp (U)$
47	27 43 45 46	syl3anc	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\}) \in LSubSp (U)$
48	1 14 2 26 16 36 47	mapdin	$⊢ φ \to M ((N (\{Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\}))) = M (N (\{Y\}) LSSum (U) N (\{Z\})) \cap M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\}))$
49		eqid	$⊢ LSSum (C) = LSSum (C)$
50	1 14 2 26 34 8 49 16 30 33	mapdlsm	$⊢ φ \to M (N (\{Y\}) LSSum (U) N (\{Z\})) = M (N (\{Y\})) LSSum (C) M (N (\{Z\}))$
51	1 2 16	dvhlvec	$⊢ φ \to U \in LVec$
52	3 6 7 51 28 21 37 23 22	lspindp2	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land \neg Z \in N (\{X, Y\}))$
53	52	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
54	1 2 3 6 7 8 9 13 14 15 16 17 19 53 18 28	hdmap1cl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
55	24 54	eqeltrrd	$⊢ φ \to G \in D$
56	1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 20 55 53 19	hdmap1eq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})))$
57	24 56	mpbid	$⊢ φ \to (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\}))$
58	57	simpld	$⊢ φ \to M (N (\{Y\})) = L (\{G\})$
59	3 6 7 51 20 31 37 23 22	lspindp1	$⊢ φ \to (N (\{X\}) \neq N (\{Z\}) \land \neg Y \in N (\{X, Z\}))$
60	59	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
61	1 2 3 6 7 8 9 13 14 15 16 17 19 60 18 31	hdmap1cl	$⊢ φ \to I (⟨X, F, Z⟩) \in D$
62	25 61	eqeltrrd	$⊢ φ \to E \in D$
63	1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 21 62 60 19	hdmap1eq	$⊢ φ \to (I (⟨X, F, Z⟩) = E \leftrightarrow (M (N (\{Z\})) = L (\{E\}) \land M (N (\{X \underset{˙}{-} Z\})) = L (\{F R E\})))$
64	25 63	mpbid	$⊢ φ \to (M (N (\{Z\})) = L (\{E\}) \land M (N (\{X \underset{˙}{-} Z\})) = L (\{F R E\}))$
65	64	simpld	$⊢ φ \to M (N (\{Z\})) = L (\{E\})$
66	58 65	oveq12d	$⊢ φ \to M (N (\{Y\})) LSSum (C) M (N (\{Z\})) = L (\{G\}) LSSum (C) L (\{E\})$
67	50 66	eqtrd	$⊢ φ \to M (N (\{Y\}) LSSum (U) N (\{Z\})) = L (\{G\}) LSSum (C) L (\{E\})$
68	1 14 2 26 34 8 49 16 43 45	mapdlsm	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\})) = M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) LSSum (C) M (N (\{X\}))$
69	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)\})$
70	69 19	oveq12d	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) LSSum (C) M (N (\{X\})) = L (\{F R (G \underset{˙}{✚} E)\}) LSSum (C) L (\{F\})$
71	68 70	eqtrd	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\})) = L (\{F R (G \underset{˙}{✚} E)\}) LSSum (C) L (\{F\})$
72	67 71	ineq12d	$⊢ φ \to M (N (\{Y\}) LSSum (U) N (\{Z\})) \cap M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\})) = (L (\{G\}) LSSum (C) L (\{E\})) \cap (L (\{F R (G \underset{˙}{✚} E)\}) LSSum (C) L (\{F\}))$
73	48 72	eqtrd	$⊢ φ \to M ((N (\{Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\}))) = (L (\{G\}) LSSum (C) L (\{E\})) \cap (L (\{F R (G \underset{˙}{✚} E)\}) LSSum (C) L (\{F\}))$
74	3 5 6 34 7 51 37 22 23 20 21 4	baerlem5b	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) = (N (\{Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\}))$
75	74	fveq2d	$⊢ φ \to M (N (\{Y \underset{˙}{+} Z\})) = M ((N (\{Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) LSSum (U) N (\{X\})))$
76	1 8 16	lcdlvec	$⊢ φ \to C \in LVec$
77	1 14 2 3 7 8 9 13 16 17 19 37 28 55 58 31 62 65 22	mapdindp	$⊢ φ \to \neg F \in L (\{G, E\})$
78	1 14 2 3 7 8 9 13 16 55 58 28 31 62 65 23	mapdncol	$⊢ φ \to L (\{G\}) \neq L (\{E\})$
79	1 14 2 3 7 8 9 13 16 55 58 6 12 20	mapdn0	$⊢ φ \to G \in (D ∖ \{Q\})$
80	1 14 2 3 7 8 9 13 16 62 65 6 12 21	mapdn0	$⊢ φ \to E \in (D ∖ \{Q\})$
81	9 11 12 49 13 76 17 77 78 79 80 10	baerlem5b	$⊢ φ \to L (\{G \underset{˙}{✚} E\}) = (L (\{G\}) LSSum (C) L (\{E\})) \cap (L (\{F R (G \underset{˙}{✚} E)\}) LSSum (C) L (\{F\}))$
82	73 75 81	3eqtr4d	$⊢ φ \to M (N (\{Y \underset{˙}{+} Z\})) = L (\{G \underset{˙}{✚} E\})$

Metamath Proof Explorer

Theorem hdmap1l6lem2

Proof