mapdindp

Description: Transfer (part of) vector independence condition from domain to range of projectivity mapd . (Contributed by NM, 11-Apr-2015)

	Ref	Expression
Hypotheses	mapdindp.h	$⊢ H = LHyp (K)$
	mapdindp.m	$⊢ M = mapd (K) (W)$
	mapdindp.u	$⊢ U = DVecH (K) (W)$
	mapdindp.v	$⊢ V = {Base}_{U}$
	mapdindp.n	$⊢ N = LSpan (U)$
	mapdindp.c	$⊢ C = LCDual (K) (W)$
	mapdindp.d	$⊢ D = {Base}_{C}$
	mapdindp.j	$⊢ J = LSpan (C)$
	mapdindp.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdindp.f	$⊢ φ \to F \in D$
	mapdindp.mx	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdindp.x	$⊢ φ \to X \in V$
	mapdindp.y	$⊢ φ \to Y \in V$
	mapdindp.g	$⊢ φ \to G \in D$
	mapdindp.my	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
	mapdindp.z	$⊢ φ \to Z \in V$
	mapdindp.e	$⊢ φ \to E \in D$
	mapdindp.mg	$⊢ φ \to M (N (\{Z\})) = J (\{E\})$
	mapdindp.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
Assertion	mapdindp	$⊢ φ \to \neg F \in J (\{G, E\})$

Proof

Step	Hyp	Ref	Expression
1		mapdindp.h	$⊢ H = LHyp (K)$
2		mapdindp.m	$⊢ M = mapd (K) (W)$
3		mapdindp.u	$⊢ U = DVecH (K) (W)$
4		mapdindp.v	$⊢ V = {Base}_{U}$
5		mapdindp.n	$⊢ N = LSpan (U)$
6		mapdindp.c	$⊢ C = LCDual (K) (W)$
7		mapdindp.d	$⊢ D = {Base}_{C}$
8		mapdindp.j	$⊢ J = LSpan (C)$
9		mapdindp.k	$⊢ φ \to (K \in HL \land W \in H)$
10		mapdindp.f	$⊢ φ \to F \in D$
11		mapdindp.mx	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
12		mapdindp.x	$⊢ φ \to X \in V$
13		mapdindp.y	$⊢ φ \to Y \in V$
14		mapdindp.g	$⊢ φ \to G \in D$
15		mapdindp.my	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
16		mapdindp.z	$⊢ φ \to Z \in V$
17		mapdindp.e	$⊢ φ \to E \in D$
18		mapdindp.mg	$⊢ φ \to M (N (\{Z\})) = J (\{E\})$
19		mapdindp.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
20		eqid	$⊢ LSubSp (C) = LSubSp (C)$
21	1 6 9	lcdlmod	$⊢ φ \to C \in LMod$
22	7 20 8 21 14 17	lspprcl	$⊢ φ \to J (\{G, E\}) \in LSubSp (C)$
23	7 20 8 21 22 10	ellspsn5b	$⊢ φ \to (F \in J (\{G, E\}) \leftrightarrow J (\{F\}) \subseteq J (\{G, E\}))$
24		eqid	$⊢ LSubSp (U) = LSubSp (U)$
25	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
26	4 24 5 25 13 16	lspprcl	$⊢ φ \to N (\{Y, Z\}) \in LSubSp (U)$
27	4 24 5 25 26 12	ellspsn5b	$⊢ φ \to (X \in N (\{Y, Z\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y, Z\}))$
28	4 24 5	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
29	25 12 28	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
30	1 3 24 2 9 29 26	mapdord	$⊢ φ \to (M (N (\{X\})) \subseteq M (N (\{Y, Z\})) \leftrightarrow N (\{X\}) \subseteq N (\{Y, Z\}))$
31		eqid	$⊢ LSSum (U) = LSSum (U)$
32	4 5 31 25 13 16	lsmpr	$⊢ φ \to N (\{Y, Z\}) = N (\{Y\}) LSSum (U) N (\{Z\})$
33	32	fveq2d	$⊢ φ \to M (N (\{Y, Z\})) = M (N (\{Y\}) LSSum (U) N (\{Z\}))$
34		eqid	$⊢ LSSum (C) = LSSum (C)$
35	4 24 5	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
36	25 13 35	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
37	4 24 5	lspsncl	$⊢ (U \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (U)$
38	25 16 37	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (U)$
39	1 2 3 24 31 6 34 9 36 38	mapdlsm	$⊢ φ \to M (N (\{Y\}) LSSum (U) N (\{Z\})) = M (N (\{Y\})) LSSum (C) M (N (\{Z\}))$
40	15 18	oveq12d	$⊢ φ \to M (N (\{Y\})) LSSum (C) M (N (\{Z\})) = J (\{G\}) LSSum (C) J (\{E\})$
41	33 39 40	3eqtrd	$⊢ φ \to M (N (\{Y, Z\})) = J (\{G\}) LSSum (C) J (\{E\})$
42	7 8 34 21 14 17	lsmpr	$⊢ φ \to J (\{G, E\}) = J (\{G\}) LSSum (C) J (\{E\})$
43	41 42	eqtr4d	$⊢ φ \to M (N (\{Y, Z\})) = J (\{G, E\})$
44	11 43	sseq12d	$⊢ φ \to (M (N (\{X\})) \subseteq M (N (\{Y, Z\})) \leftrightarrow J (\{F\}) \subseteq J (\{G, E\}))$
45	27 30 44	3bitr2rd	$⊢ φ \to (J (\{F\}) \subseteq J (\{G, E\}) \leftrightarrow X \in N (\{Y, Z\}))$
46	23 45	bitrd	$⊢ φ \to (F \in J (\{G, E\}) \leftrightarrow X \in N (\{Y, Z\}))$
47	19 46	mtbird	$⊢ φ \to \neg F \in J (\{G, E\})$

Metamath Proof Explorer

Theorem mapdindp

Proof