mapdheq4lem

Description: Lemma for mapdheq4 . Part (4) in Baer p. 46. (Contributed by NM, 12-Apr-2015)

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

Metamath Proof Explorer

Theorem mapdheq4lem

Proof