mapdpglem1

Description: Lemma for mapdpg . Baer p. 44, last line: "(F(x-y))* <= (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015)

	Ref	Expression
Hypotheses	mapdpglem.h	$⊢ H = LHyp (K)$
	mapdpglem.m	$⊢ M = mapd (K) (W)$
	mapdpglem.u	$⊢ U = DVecH (K) (W)$
	mapdpglem.v	$⊢ V = {Base}_{U}$
	mapdpglem.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdpglem.n	$⊢ N = LSpan (U)$
	mapdpglem.c	$⊢ C = LCDual (K) (W)$
	mapdpglem.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdpglem.x	$⊢ φ \to X \in V$
	mapdpglem.y	$⊢ φ \to Y \in V$
	mapdpglem1.p	$⊢ \underset{˙}{\oplus} = LSSum (C)$
Assertion	mapdpglem1	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) \subseteq M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))$

Proof

Step	Hyp	Ref	Expression
1		mapdpglem.h	$⊢ H = LHyp (K)$
2		mapdpglem.m	$⊢ M = mapd (K) (W)$
3		mapdpglem.u	$⊢ U = DVecH (K) (W)$
4		mapdpglem.v	$⊢ V = {Base}_{U}$
5		mapdpglem.s	$⊢ \underset{˙}{-} = -_{U}$
6		mapdpglem.n	$⊢ N = LSpan (U)$
7		mapdpglem.c	$⊢ C = LCDual (K) (W)$
8		mapdpglem.k	$⊢ φ \to (K \in HL \land W \in H)$
9		mapdpglem.x	$⊢ φ \to X \in V$
10		mapdpglem.y	$⊢ φ \to Y \in V$
11		mapdpglem1.p	$⊢ \underset{˙}{\oplus} = LSSum (C)$
12	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
13		eqid	$⊢ LSSum (U) = LSSum (U)$
14	4 5 13 6	lspsntrim	$⊢ (U \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{-} Y\}) \subseteq N (\{X\}) LSSum (U) N (\{Y\})$
15	12 9 10 14	syl3anc	$⊢ φ \to N (\{X \underset{˙}{-} Y\}) \subseteq N (\{X\}) LSSum (U) N (\{Y\})$
16		eqid	$⊢ LSubSp (U) = LSubSp (U)$
17	4 5	lmodvsubcl	$⊢ (U \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{-} Y \in V$
18	12 9 10 17	syl3anc	$⊢ φ \to X \underset{˙}{-} Y \in V$
19	4 16 6	lspsncl	$⊢ (U \in LMod \land X \underset{˙}{-} Y \in V) \to N (\{X \underset{˙}{-} Y\}) \in LSubSp (U)$
20	12 18 19	syl2anc	$⊢ φ \to N (\{X \underset{˙}{-} Y\}) \in LSubSp (U)$
21	4 16 6	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
22	12 9 21	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
23	4 16 6	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
24	12 10 23	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
25	16 13	lsmcl	$⊢ (U \in LMod \land N (\{X\}) \in LSubSp (U) \land N (\{Y\}) \in LSubSp (U)) \to N (\{X\}) LSSum (U) N (\{Y\}) \in LSubSp (U)$
26	12 22 24 25	syl3anc	$⊢ φ \to N (\{X\}) LSSum (U) N (\{Y\}) \in LSubSp (U)$
27	1 3 16 2 8 20 26	mapdord	$⊢ φ \to (M (N (\{X \underset{˙}{-} Y\})) \subseteq M (N (\{X\}) LSSum (U) N (\{Y\})) \leftrightarrow N (\{X \underset{˙}{-} Y\}) \subseteq N (\{X\}) LSSum (U) N (\{Y\}))$
28	15 27	mpbird	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) \subseteq M (N (\{X\}) LSSum (U) N (\{Y\}))$
29	1 2 3 16 13 7 11 8 22 24	mapdlsm	$⊢ φ \to M (N (\{X\}) LSSum (U) N (\{Y\})) = M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))$
30	28 29	sseqtrd	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) \subseteq M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))$

Metamath Proof Explorer

Theorem mapdpglem1

Proof