mapdh6lem1N

Description: Lemma for mapdh6N . Part (6) in Baer p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh.q	$⊢ Q = 0_{C}$
	mapdh.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	mapdh.h	$⊢ H = LHyp (K)$
	mapdh.m	$⊢ M = mapd (K) (W)$
	mapdh.u	$⊢ U = DVecH (K) (W)$
	mapdh.v	$⊢ V = {Base}_{U}$
	mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdh.n	$⊢ N = LSpan (U)$
	mapdh.c	$⊢ C = LCDual (K) (W)$
	mapdh.d	$⊢ D = {Base}_{C}$
	mapdh.r	$⊢ R = -_{C}$
	mapdh.j	$⊢ J = LSpan (C)$
	mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdhc.f	$⊢ φ \to F \in D$
	mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh.p	$⊢ \underset{˙}{+} = +_{U}$
	mapdh.a	$⊢ \underset{˙}{✚} = +_{C}$
	mapdhe6.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdhe6.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdhe6.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	mapdh6.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
	mapdh6.fg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh6.fe	$⊢ φ \to I (⟨X, F, Z⟩) = E$
Assertion	mapdh6lem1N	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) = J (\{F R (G \underset{˙}{✚} E)\})$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$⊢ Q = 0_{C}$
2		mapdh.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
3		mapdh.h	$⊢ H = LHyp (K)$
4		mapdh.m	$⊢ M = mapd (K) (W)$
5		mapdh.u	$⊢ U = DVecH (K) (W)$
6		mapdh.v	$⊢ V = {Base}_{U}$
7		mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
8		mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
9		mapdh.n	$⊢ N = LSpan (U)$
10		mapdh.c	$⊢ C = LCDual (K) (W)$
11		mapdh.d	$⊢ D = {Base}_{C}$
12		mapdh.r	$⊢ R = -_{C}$
13		mapdh.j	$⊢ J = LSpan (C)$
14		mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
15		mapdhc.f	$⊢ φ \to F \in D$
16		mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		mapdh.p	$⊢ \underset{˙}{+} = +_{U}$
19		mapdh.a	$⊢ \underset{˙}{✚} = +_{C}$
20		mapdhe6.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
21		mapdhe6.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
22		mapdhe6.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
23		mapdh6.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
24		mapdh6.fg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
25		mapdh6.fe	$⊢ φ \to I (⟨X, F, Z⟩) = E$
26		eqid	$⊢ LSubSp (U) = LSubSp (U)$
27	3 5 14	dvhlmod	$⊢ φ \to U \in LMod$
28	17	eldifad	$⊢ φ \to X \in V$
29	20	eldifad	$⊢ φ \to Y \in V$
30	6 7	lmodvsubcl	$⊢ (U \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{-} Y \in V$
31	27 28 29 30	syl3anc	$⊢ φ \to X \underset{˙}{-} Y \in V$
32	6 26 9	lspsncl	$⊢ (U \in LMod \land X \underset{˙}{-} Y \in V) \to N (\{X \underset{˙}{-} Y\}) \in LSubSp (U)$
33	27 31 32	syl2anc	$⊢ φ \to N (\{X \underset{˙}{-} Y\}) \in LSubSp (U)$
34	21	eldifad	$⊢ φ \to Z \in V$
35	6 26 9	lspsncl	$⊢ (U \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (U)$
36	27 34 35	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (U)$
37		eqid	$⊢ LSSum (U) = LSSum (U)$
38	26 37	lsmcl	$⊢ (U \in LMod \land N (\{X \underset{˙}{-} Y\}) \in LSubSp (U) \land N (\{Z\}) \in LSubSp (U)) \to N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\}) \in LSubSp (U)$
39	27 33 36 38	syl3anc	$⊢ φ \to N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\}) \in LSubSp (U)$
40	6 7	lmodvsubcl	$⊢ (U \in LMod \land X \in V \land Z \in V) \to X \underset{˙}{-} Z \in V$
41	27 28 34 40	syl3anc	$⊢ φ \to X \underset{˙}{-} Z \in V$
42	6 26 9	lspsncl	$⊢ (U \in LMod \land X \underset{˙}{-} Z \in V) \to N (\{X \underset{˙}{-} Z\}) \in LSubSp (U)$
43	27 41 42	syl2anc	$⊢ φ \to N (\{X \underset{˙}{-} Z\}) \in LSubSp (U)$
44	6 26 9	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
45	27 29 44	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
46	26 37	lsmcl	$⊢ (U \in LMod \land N (\{X \underset{˙}{-} Z\}) \in LSubSp (U) \land N (\{Y\}) \in LSubSp (U)) \to N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\}) \in LSubSp (U)$
47	27 43 45 46	syl3anc	$⊢ φ \to N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\}) \in LSubSp (U)$
48	3 4 5 26 14 39 47	mapdin	$⊢ φ \to M ((N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\}))) = M (N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap M (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\}))$
49		eqid	$⊢ LSSum (C) = LSSum (C)$
50	3 4 5 26 37 10 49 14 33 36	mapdlsm	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) = M (N (\{X \underset{˙}{-} Y\})) LSSum (C) M (N (\{Z\}))$
51	3 4 5 26 37 10 49 14 43 45	mapdlsm	$⊢ φ \to M (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\})) = M (N (\{X \underset{˙}{-} Z\})) LSSum (C) M (N (\{Y\}))$
52	50 51	ineq12d	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap M (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\})) = (M (N (\{X \underset{˙}{-} Y\})) LSSum (C) M (N (\{Z\}))) \cap (M (N (\{X \underset{˙}{-} Z\})) LSSum (C) M (N (\{Y\})))$
53	3 5 14	dvhlvec	$⊢ φ \to U \in LVec$
54	6 8 9 53 29 21 28 23 22	lspindp2	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land \neg Z \in N (\{X, Y\}))$
55	54	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
56	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 29 55	mapdhcl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
57	24 56	eqeltrrd	$⊢ φ \to G \in D$
58	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 20 57 55	mapdheq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})))$
59	24 58	mpbid	$⊢ φ \to (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))$
60	59	simprd	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})$
61	6 8 9 53 20 34 28 23 22	lspindp1	$⊢ φ \to (N (\{X\}) \neq N (\{Z\}) \land \neg Y \in N (\{X, Z\}))$
62	61	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
63	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 34 62	mapdhcl	$⊢ φ \to I (⟨X, F, Z⟩) \in D$
64	25 63	eqeltrrd	$⊢ φ \to E \in D$
65	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 21 64 62	mapdheq	$⊢ φ \to (I (⟨X, F, Z⟩) = E \leftrightarrow (M (N (\{Z\})) = J (\{E\}) \land M (N (\{X \underset{˙}{-} Z\})) = J (\{F R E\})))$
66	25 65	mpbid	$⊢ φ \to (M (N (\{Z\})) = J (\{E\}) \land M (N (\{X \underset{˙}{-} Z\})) = J (\{F R E\}))$
67	66	simpld	$⊢ φ \to M (N (\{Z\})) = J (\{E\})$
68	60 67	oveq12d	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) LSSum (C) M (N (\{Z\})) = J (\{F R G\}) LSSum (C) J (\{E\})$
69	66	simprd	$⊢ φ \to M (N (\{X \underset{˙}{-} Z\})) = J (\{F R E\})$
70	59	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
71	69 70	oveq12d	$⊢ φ \to M (N (\{X \underset{˙}{-} Z\})) LSSum (C) M (N (\{Y\})) = J (\{F R E\}) LSSum (C) J (\{G\})$
72	68 71	ineq12d	$⊢ φ \to (M (N (\{X \underset{˙}{-} Y\})) LSSum (C) M (N (\{Z\}))) \cap (M (N (\{X \underset{˙}{-} Z\})) LSSum (C) M (N (\{Y\}))) = (J (\{F R G\}) LSSum (C) J (\{E\})) \cap (J (\{F R E\}) LSSum (C) J (\{G\}))$
73	52 72	eqtrd	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap M (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\})) = (J (\{F R G\}) LSSum (C) J (\{E\})) \cap (J (\{F R E\}) LSSum (C) J (\{G\}))$
74	48 73	eqtrd	$⊢ φ \to M ((N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\}))) = (J (\{F R G\}) LSSum (C) J (\{E\})) \cap (J (\{F R E\}) LSSum (C) J (\{G\}))$
75	6 7 8 37 9 53 28 22 23 20 21 18	baerlem5a	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\}) = (N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\}))$
76	75	fveq2d	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) = M ((N (\{X \underset{˙}{-} Y\}) LSSum (U) N (\{Z\})) \cap (N (\{X \underset{˙}{-} Z\}) LSSum (U) N (\{Y\})))$
77	3 10 14	lcdlvec	$⊢ φ \to C \in LVec$
78	3 4 5 6 9 10 11 13 14 15 16 28 29 57 70 34 64 67 22	mapdindp	$⊢ φ \to \neg F \in J (\{G, E\})$
79	3 4 5 6 9 10 11 13 14 57 70 29 34 64 67 23	mapdncol	$⊢ φ \to J (\{G\}) \neq J (\{E\})$
80	3 4 5 6 9 10 11 13 14 57 70 8 1 20	mapdn0	$⊢ φ \to G \in (D ∖ \{Q\})$
81	3 4 5 6 9 10 11 13 14 64 67 8 1 21	mapdn0	$⊢ φ \to E \in (D ∖ \{Q\})$
82	11 12 1 49 13 77 15 78 79 80 81 19	baerlem5a	$⊢ φ \to J (\{F R (G \underset{˙}{✚} E)\}) = (J (\{F R G\}) LSSum (C) J (\{E\})) \cap (J (\{F R E\}) LSSum (C) J (\{G\}))$
83	74 76 82	3eqtr4d	$⊢ φ \to M (N (\{X \underset{˙}{-} (Y \underset{˙}{+} Z)\})) = J (\{F R (G \underset{˙}{✚} E)\})$

Metamath Proof Explorer

Theorem mapdh6lem1N

Proof