mapdlsm

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

	Ref	Expression
Hypotheses	mapdlsm.h	$⊢ H = LHyp (K)$
	mapdlsm.m	$⊢ M = mapd (K) (W)$
	mapdlsm.u	$⊢ U = DVecH (K) (W)$
	mapdlsm.s	$⊢ S = LSubSp (U)$
	mapdlsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	mapdlsm.c	$⊢ C = LCDual (K) (W)$
	mapdlsm.q	$⊢ \underset{˙}{✚} = LSSum (C)$
	mapdlsm.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdlsm.x	$⊢ φ \to X \in S$
	mapdlsm.y	$⊢ φ \to Y \in S$
Assertion	mapdlsm	$⊢ φ \to M (X \underset{˙}{\oplus} Y) = M (X) \underset{˙}{✚} M (Y)$

Proof

Step	Hyp	Ref	Expression
1		mapdlsm.h	$⊢ H = LHyp (K)$
2		mapdlsm.m	$⊢ M = mapd (K) (W)$
3		mapdlsm.u	$⊢ U = DVecH (K) (W)$
4		mapdlsm.s	$⊢ S = LSubSp (U)$
5		mapdlsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
6		mapdlsm.c	$⊢ C = LCDual (K) (W)$
7		mapdlsm.q	$⊢ \underset{˙}{✚} = LSSum (C)$
8		mapdlsm.k	$⊢ φ \to (K \in HL \land W \in H)$
9		mapdlsm.x	$⊢ φ \to X \in S$
10		mapdlsm.y	$⊢ φ \to Y \in S$
11	1 6 8	lcdlmod	$⊢ φ \to C \in LMod$
12		eqid	$⊢ LSubSp (C) = LSubSp (C)$
13	12	lsssssubg	$⊢ C \in LMod \to LSubSp (C) \subseteq SubGrp (C)$
14	11 13	syl	$⊢ φ \to LSubSp (C) \subseteq SubGrp (C)$
15	1 2 3 4 6 12 8 9	mapdcl2	$⊢ φ \to M (X) \in LSubSp (C)$
16	14 15	sseldd	$⊢ φ \to M (X) \in SubGrp (C)$
17	1 2 3 4 6 12 8 10	mapdcl2	$⊢ φ \to M (Y) \in LSubSp (C)$
18	14 17	sseldd	$⊢ φ \to M (Y) \in SubGrp (C)$
19	7	lsmub1	$⊢ (M (X) \in SubGrp (C) \land M (Y) \in SubGrp (C)) \to M (X) \subseteq M (X) \underset{˙}{✚} M (Y)$
20	16 18 19	syl2anc	$⊢ φ \to M (X) \subseteq M (X) \underset{˙}{✚} M (Y)$
21	1 2 3 4 8 9	mapdcl	$⊢ φ \to M (X) \in ran M$
22	1 2 3 4 8 10	mapdcl	$⊢ φ \to M (Y) \in ran M$
23	1 2 3 6 7 8 21 22	mapdlsmcl	$⊢ φ \to M (X) \underset{˙}{✚} M (Y) \in ran M$
24	1 2 8 23	mapdcnvid2	$⊢ φ \to M (M^{-1} (M (X) \underset{˙}{✚} M (Y))) = M (X) \underset{˙}{✚} M (Y)$
25	20 24	sseqtrrd	$⊢ φ \to M (X) \subseteq M (M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
26	1 2 3 4 8 23	mapdcnvcl	$⊢ φ \to M^{-1} (M (X) \underset{˙}{✚} M (Y)) \in S$
27	1 3 4 2 8 9 26	mapdord	$⊢ φ \to (M (X) \subseteq M (M^{-1} (M (X) \underset{˙}{✚} M (Y))) \leftrightarrow X \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
28	25 27	mpbid	$⊢ φ \to X \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y))$
29	7	lsmub2	$⊢ (M (X) \in SubGrp (C) \land M (Y) \in SubGrp (C)) \to M (Y) \subseteq M (X) \underset{˙}{✚} M (Y)$
30	16 18 29	syl2anc	$⊢ φ \to M (Y) \subseteq M (X) \underset{˙}{✚} M (Y)$
31	30 24	sseqtrrd	$⊢ φ \to M (Y) \subseteq M (M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
32	1 3 4 2 8 10 26	mapdord	$⊢ φ \to (M (Y) \subseteq M (M^{-1} (M (X) \underset{˙}{✚} M (Y))) \leftrightarrow Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
33	31 32	mpbid	$⊢ φ \to Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y))$
34	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
35	4	lsssssubg	$⊢ U \in LMod \to S \subseteq SubGrp (U)$
36	34 35	syl	$⊢ φ \to S \subseteq SubGrp (U)$
37	36 9	sseldd	$⊢ φ \to X \in SubGrp (U)$
38	36 10	sseldd	$⊢ φ \to Y \in SubGrp (U)$
39	36 26	sseldd	$⊢ φ \to M^{-1} (M (X) \underset{˙}{✚} M (Y)) \in SubGrp (U)$
40	5	lsmlub	$⊢ (X \in SubGrp (U) \land Y \in SubGrp (U) \land M^{-1} (M (X) \underset{˙}{✚} M (Y)) \in SubGrp (U)) \to ((X \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)) \land Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y))) \leftrightarrow X \underset{˙}{\oplus} Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
41	37 38 39 40	syl3anc	$⊢ φ \to ((X \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)) \land Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y))) \leftrightarrow X \underset{˙}{\oplus} Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
42	28 33 41	mpbi2and	$⊢ φ \to X \underset{˙}{\oplus} Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y))$
43	4 5	lsmcl	$⊢ (U \in LMod \land X \in S \land Y \in S) \to X \underset{˙}{\oplus} Y \in S$
44	34 9 10 43	syl3anc	$⊢ φ \to X \underset{˙}{\oplus} Y \in S$
45	1 3 4 2 8 44 26	mapdord	$⊢ φ \to (M (X \underset{˙}{\oplus} Y) \subseteq M (M^{-1} (M (X) \underset{˙}{✚} M (Y))) \leftrightarrow X \underset{˙}{\oplus} Y \subseteq M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
46	42 45	mpbird	$⊢ φ \to M (X \underset{˙}{\oplus} Y) \subseteq M (M^{-1} (M (X) \underset{˙}{✚} M (Y)))$
47	46 24	sseqtrd	$⊢ φ \to M (X \underset{˙}{\oplus} Y) \subseteq M (X) \underset{˙}{✚} M (Y)$
48	5	lsmub1	$⊢ (X \in SubGrp (U) \land Y \in SubGrp (U)) \to X \subseteq X \underset{˙}{\oplus} Y$
49	37 38 48	syl2anc	$⊢ φ \to X \subseteq X \underset{˙}{\oplus} Y$
50	1 3 4 2 8 9 44	mapdord	$⊢ φ \to (M (X) \subseteq M (X \underset{˙}{\oplus} Y) \leftrightarrow X \subseteq X \underset{˙}{\oplus} Y)$
51	49 50	mpbird	$⊢ φ \to M (X) \subseteq M (X \underset{˙}{\oplus} Y)$
52	5	lsmub2	$⊢ (X \in SubGrp (U) \land Y \in SubGrp (U)) \to Y \subseteq X \underset{˙}{\oplus} Y$
53	37 38 52	syl2anc	$⊢ φ \to Y \subseteq X \underset{˙}{\oplus} Y$
54	1 3 4 2 8 10 44	mapdord	$⊢ φ \to (M (Y) \subseteq M (X \underset{˙}{\oplus} Y) \leftrightarrow Y \subseteq X \underset{˙}{\oplus} Y)$
55	53 54	mpbird	$⊢ φ \to M (Y) \subseteq M (X \underset{˙}{\oplus} Y)$
56	1 2 3 4 6 12 8 44	mapdcl2	$⊢ φ \to M (X \underset{˙}{\oplus} Y) \in LSubSp (C)$
57	14 56	sseldd	$⊢ φ \to M (X \underset{˙}{\oplus} Y) \in SubGrp (C)$
58	7	lsmlub	$⊢ (M (X) \in SubGrp (C) \land M (Y) \in SubGrp (C) \land M (X \underset{˙}{\oplus} Y) \in SubGrp (C)) \to ((M (X) \subseteq M (X \underset{˙}{\oplus} Y) \land M (Y) \subseteq M (X \underset{˙}{\oplus} Y)) \leftrightarrow M (X) \underset{˙}{✚} M (Y) \subseteq M (X \underset{˙}{\oplus} Y))$
59	16 18 57 58	syl3anc	$⊢ φ \to ((M (X) \subseteq M (X \underset{˙}{\oplus} Y) \land M (Y) \subseteq M (X \underset{˙}{\oplus} Y)) \leftrightarrow M (X) \underset{˙}{✚} M (Y) \subseteq M (X \underset{˙}{\oplus} Y))$
60	51 55 59	mpbi2and	$⊢ φ \to M (X) \underset{˙}{✚} M (Y) \subseteq M (X \underset{˙}{\oplus} Y)$
61	47 60	eqssd	$⊢ φ \to M (X \underset{˙}{\oplus} Y) = M (X) \underset{˙}{✚} M (Y)$

Metamath Proof Explorer

Theorem mapdlsm

Proof