mapdin

Description: Subspace intersection is preserved by the map defined by df-mapd . Part of property (e) in Baer p. 40. (Contributed by NM, 12-Apr-2015)

	Ref	Expression
Hypotheses	mapdin.h	$⊢ H = LHyp (K)$
	mapdin.m	$⊢ M = mapd (K) (W)$
	mapdin.u	$⊢ U = DVecH (K) (W)$
	mapdin.s	$⊢ S = LSubSp (U)$
	mapdin.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdin.x	$⊢ φ \to X \in S$
	mapdin.y	$⊢ φ \to Y \in S$
Assertion	mapdin	$⊢ φ \to M (X \cap Y) = M (X) \cap M (Y)$

Proof

Step	Hyp	Ref	Expression
1		mapdin.h	$⊢ H = LHyp (K)$
2		mapdin.m	$⊢ M = mapd (K) (W)$
3		mapdin.u	$⊢ U = DVecH (K) (W)$
4		mapdin.s	$⊢ S = LSubSp (U)$
5		mapdin.k	$⊢ φ \to (K \in HL \land W \in H)$
6		mapdin.x	$⊢ φ \to X \in S$
7		mapdin.y	$⊢ φ \to Y \in S$
8		inss1	$⊢ X \cap Y \subseteq X$
9	1 3 5	dvhlmod	$⊢ φ \to U \in LMod$
10	4	lssincl	$⊢ (U \in LMod \land X \in S \land Y \in S) \to X \cap Y \in S$
11	9 6 7 10	syl3anc	$⊢ φ \to X \cap Y \in S$
12	1 3 4 2 5 11 6	mapdord	$⊢ φ \to (M (X \cap Y) \subseteq M (X) \leftrightarrow X \cap Y \subseteq X)$
13	8 12	mpbiri	$⊢ φ \to M (X \cap Y) \subseteq M (X)$
14		inss2	$⊢ X \cap Y \subseteq Y$
15	1 3 4 2 5 11 7	mapdord	$⊢ φ \to (M (X \cap Y) \subseteq M (Y) \leftrightarrow X \cap Y \subseteq Y)$
16	14 15	mpbiri	$⊢ φ \to M (X \cap Y) \subseteq M (Y)$
17	13 16	ssind	$⊢ φ \to M (X \cap Y) \subseteq M (X) \cap M (Y)$
18		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
19		eqid	$⊢ LSubSp (LCDual (K) (W)) = LSubSp (LCDual (K) (W))$
20	1 2 3 4 18 19 5 6	mapdcl2	$⊢ φ \to M (X) \in LSubSp (LCDual (K) (W))$
21	1 2 18 19 5	mapdrn2	$⊢ φ \to ran M = LSubSp (LCDual (K) (W))$
22	20 21	eleqtrrd	$⊢ φ \to M (X) \in ran M$
23	1 2 3 4 18 19 5 7	mapdcl2	$⊢ φ \to M (Y) \in LSubSp (LCDual (K) (W))$
24	23 21	eleqtrrd	$⊢ φ \to M (Y) \in ran M$
25	1 2 3 18 5 22 24	mapdincl	$⊢ φ \to M (X) \cap M (Y) \in ran M$
26	1 2 5 25	mapdcnvid2	$⊢ φ \to M (M^{-1} (M (X) \cap M (Y))) = M (X) \cap M (Y)$
27		inss1	$⊢ M (X) \cap M (Y) \subseteq M (X)$
28	26 27	eqsstrdi	$⊢ φ \to M (M^{-1} (M (X) \cap M (Y))) \subseteq M (X)$
29	1 18 5	lcdlmod	$⊢ φ \to LCDual (K) (W) \in LMod$
30	19	lssincl	$⊢ (LCDual (K) (W) \in LMod \land M (X) \in LSubSp (LCDual (K) (W)) \land M (Y) \in LSubSp (LCDual (K) (W))) \to M (X) \cap M (Y) \in LSubSp (LCDual (K) (W))$
31	29 20 23 30	syl3anc	$⊢ φ \to M (X) \cap M (Y) \in LSubSp (LCDual (K) (W))$
32	31 21	eleqtrrd	$⊢ φ \to M (X) \cap M (Y) \in ran M$
33	1 2 3 4 5 32	mapdcnvcl	$⊢ φ \to M^{-1} (M (X) \cap M (Y)) \in S$
34	1 3 4 2 5 33 6	mapdord	$⊢ φ \to (M (M^{-1} (M (X) \cap M (Y))) \subseteq M (X) \leftrightarrow M^{-1} (M (X) \cap M (Y)) \subseteq X)$
35	28 34	mpbid	$⊢ φ \to M^{-1} (M (X) \cap M (Y)) \subseteq X$
36	1 2 5 32	mapdcnvid2	$⊢ φ \to M (M^{-1} (M (X) \cap M (Y))) = M (X) \cap M (Y)$
37		inss2	$⊢ M (X) \cap M (Y) \subseteq M (Y)$
38	36 37	eqsstrdi	$⊢ φ \to M (M^{-1} (M (X) \cap M (Y))) \subseteq M (Y)$
39	1 3 4 2 5 33 7	mapdord	$⊢ φ \to (M (M^{-1} (M (X) \cap M (Y))) \subseteq M (Y) \leftrightarrow M^{-1} (M (X) \cap M (Y)) \subseteq Y)$
40	38 39	mpbid	$⊢ φ \to M^{-1} (M (X) \cap M (Y)) \subseteq Y$
41	35 40	ssind	$⊢ φ \to M^{-1} (M (X) \cap M (Y)) \subseteq X \cap Y$
42	1 3 4 2 5 33 11	mapdord	$⊢ φ \to (M (M^{-1} (M (X) \cap M (Y))) \subseteq M (X \cap Y) \leftrightarrow M^{-1} (M (X) \cap M (Y)) \subseteq X \cap Y)$
43	41 42	mpbird	$⊢ φ \to M (M^{-1} (M (X) \cap M (Y))) \subseteq M (X \cap Y)$
44	26 43	eqsstrrd	$⊢ φ \to M (X) \cap M (Y) \subseteq M (X \cap Y)$
45	17 44	eqssd	$⊢ φ \to M (X \cap Y) = M (X) \cap M (Y)$

Metamath Proof Explorer

Theorem mapdin

Proof