mapdpglem2

Description: Lemma for mapdpg . Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d t ph locally to avoid clashes with later substitutions into ph .) (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)$
	mapdpglem2.j	$⊢ J = LSpan (C)$
Assertion	mapdpglem2	$⊢ φ \to \exists t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$

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		mapdpglem2.j	$⊢ J = LSpan (C)$
13		eqid	$⊢ {Base}_{C} = {Base}_{C}$
14	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
15	4 5	lmodvsubcl	$⊢ (U \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{-} Y \in V$
16	14 9 10 15	syl3anc	$⊢ φ \to X \underset{˙}{-} Y \in V$
17	1 2 3 4 6 7 13 12 8 16	mapdspex	$⊢ φ \to \exists t \in {Base}_{C} M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
18	1 7 8	lcdlmod	$⊢ φ \to C \in LMod$
19	13 12	lspsnid	$⊢ (C \in LMod \land t \in {Base}_{C}) \to t \in J (\{t\})$
20	18 19	sylan	$⊢ (φ \land t \in {Base}_{C}) \to t \in J (\{t\})$
21	20	adantrr	$⊢ (φ \land (t \in {Base}_{C} \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\}))) \to t \in J (\{t\})$
22		simprr	$⊢ (φ \land (t \in {Base}_{C} \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\}))) \to M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
23	21 22	eleqtrrd	$⊢ (φ \land (t \in {Base}_{C} \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\}))) \to t \in M (N (\{X \underset{˙}{-} Y\}))$
24	17 23 22	reximssdv	$⊢ φ \to \exists t \in M (N (\{X \underset{˙}{-} Y\})) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
25	1 2 3 4 5 6 7 8 9 10 11	mapdpglem1	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) \subseteq M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))$
26	25	sseld	$⊢ φ \to (t \in M (N (\{X \underset{˙}{-} Y\})) \to t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))))$
27	26	anim1d	$⊢ φ \to ((t \in M (N (\{X \underset{˙}{-} Y\})) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to (t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})))$
28	27	reximdv2	$⊢ φ \to (\exists t \in M (N (\{X \underset{˙}{-} Y\})) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\}) \to \exists t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\}))$
29	24 28	mpd	$⊢ φ \to \exists t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\}))) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$

Metamath Proof Explorer

Theorem mapdpglem2

Proof