mapdpglem24

Description: Lemma for mapdpg . Existence part - consolidate hypotheses in mapdpglem23 . (Contributed by NM, 21-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	$⊢ H = LHyp (K)$
	mapdpg.m	$⊢ M = mapd (K) (W)$
	mapdpg.u	$⊢ U = DVecH (K) (W)$
	mapdpg.v	$⊢ V = {Base}_{U}$
	mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
	mapdpg.n	$⊢ N = LSpan (U)$
	mapdpg.c	$⊢ C = LCDual (K) (W)$
	mapdpg.f	$⊢ F = {Base}_{C}$
	mapdpg.r	$⊢ R = -_{C}$
	mapdpg.j	$⊢ J = LSpan (C)$
	mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.g	$⊢ φ \to G \in F$
	mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
Assertion	mapdpglem24	$⊢ φ \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	$⊢ H = LHyp (K)$
2		mapdpg.m	$⊢ M = mapd (K) (W)$
3		mapdpg.u	$⊢ U = DVecH (K) (W)$
4		mapdpg.v	$⊢ V = {Base}_{U}$
5		mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
6		mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
7		mapdpg.n	$⊢ N = LSpan (U)$
8		mapdpg.c	$⊢ C = LCDual (K) (W)$
9		mapdpg.f	$⊢ F = {Base}_{C}$
10		mapdpg.r	$⊢ R = -_{C}$
11		mapdpg.j	$⊢ J = LSpan (C)$
12		mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
13		mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
14		mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
15		mapdpg.g	$⊢ φ \to G \in F$
16		mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
17		mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
18	13	eldifad	$⊢ φ \to X \in V$
19	14	eldifad	$⊢ φ \to Y \in V$
20		eqid	$⊢ LSSum (C) = LSSum (C)$
21	1 2 3 4 5 7 8 12 18 19 20 11	mapdpglem2	$⊢ φ \to \exists t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
22	12	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to (K \in HL \land W \in H)$
23	18	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to X \in V$
24	19	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to Y \in V$
25		simp2	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\})))$
26		eqid	$⊢ Scalar (U) = Scalar (U)$
27		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
28		eqid	$⊢ \cdot_{C} = \cdot_{C}$
29	15	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to G \in F$
30	17	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to M (N (\{X\})) = J (\{G\})$
31	1 2 3 4 5 7 8 22 23 24 20 11 9 25 26 27 28 10 29 30	mapdpglem3	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to \exists g \in {Base}_{Scalar (U)} \exists z \in M (N (\{Y\})) t = (g \cdot_{C} G) R z$
32	22	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to (K \in HL \land W \in H)$
33	23	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to X \in V$
34	24	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to Y \in V$
35		simp12	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\})))$
36	29	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to G \in F$
37	30	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to M (N (\{X\})) = J (\{G\})$
38	16	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to N (\{X\}) \neq N (\{Y\})$
39	38	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to N (\{X\}) \neq N (\{Y\})$
40		simp13	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
41		eqid	$⊢ 0_{Scalar (U)} = 0_{Scalar (U)}$
42		simp2l	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to g \in {Base}_{Scalar (U)}$
43		simp2r	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to z \in M (N (\{Y\}))$
44		simp3	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to t = (g \cdot_{C} G) R z$
45		eldifsni	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
46	13 45	syl	$⊢ φ \to X \neq \underset{˙}{0}$
47	46	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to X \neq \underset{˙}{0}$
48	47	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to X \neq \underset{˙}{0}$
49		eldifsni	$⊢ Y \in (V ∖ \{\underset{˙}{0}\}) \to Y \neq \underset{˙}{0}$
50	14 49	syl	$⊢ φ \to Y \neq \underset{˙}{0}$
51	50	3ad2ant1	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to Y \neq \underset{˙}{0}$
52	51	3ad2ant1	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to Y \neq \underset{˙}{0}$
53		eqid	$⊢ {inv}_{r} (Scalar (U)) (g) \cdot_{C} z = {inv}_{r} (Scalar (U)) (g) \cdot_{C} z$
54	1 2 3 4 5 7 8 32 33 34 20 11 9 35 26 27 28 10 36 37 6 39 40 41 42 43 44 48 52 53	mapdpglem23	$⊢ ((φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \land (g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \land t = (g \cdot_{C} G) R z) \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$
55	54	3exp	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to ((g \in {Base}_{Scalar (U)} \land z \in M (N (\{Y\}))) \to (t = (g \cdot_{C} G) R z \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))))$
56	55	rexlimdvv	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to (\exists g \in {Base}_{Scalar (U)} \exists z \in M (N (\{Y\})) t = (g \cdot_{C} G) R z \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
57	31 56	mpd	$⊢ (φ \land t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})) \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$
58	57	rexlimdv3a	$⊢ φ \to (\exists t \in (M (N (\{X\})) LSSum (C) M (N (\{Y\}))) M (N (\{X \underset{˙}{-} Y\})) = J (\{t\}) \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
59	21 58	mpd	$⊢ φ \to \exists h \in F (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$

Metamath Proof Explorer

Theorem mapdpglem24

Proof