mapdh8e

Description: Part of Part (8) in Baer p. 48. Eliminate w . (Contributed by NM, 10-May-2015)

	Ref	Expression
Hypotheses	mapdh8a.h	$⊢ H = LHyp (K)$
	mapdh8a.u	$⊢ U = DVecH (K) (W)$
	mapdh8a.v	$⊢ V = {Base}_{U}$
	mapdh8a.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdh8a.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdh8a.n	$⊢ N = LSpan (U)$
	mapdh8a.c	$⊢ C = LCDual (K) (W)$
	mapdh8a.d	$⊢ D = {Base}_{C}$
	mapdh8a.r	$⊢ R = -_{C}$
	mapdh8a.q	$⊢ Q = 0_{C}$
	mapdh8a.j	$⊢ J = LSpan (C)$
	mapdh8a.m	$⊢ M = mapd (K) (W)$
	mapdh8a.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	mapdh8a.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdh8e.f	$⊢ φ \to F \in D$
	mapdh8e.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh8e.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh8e.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8e.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8e.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8e.xy	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdh8e.xt	$⊢ φ \to N (\{X\}) \neq N (\{T\})$
	mapdh8e.yt	$⊢ φ \to N (\{Y\}) \neq N (\{T\})$
	mapdh8e.e	$⊢ φ \to X \in N (\{Y, T\})$
Assertion	mapdh8e	$⊢ φ \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩)$

Proof

Step	Hyp	Ref	Expression
1		mapdh8a.h	$⊢ H = LHyp (K)$
2		mapdh8a.u	$⊢ U = DVecH (K) (W)$
3		mapdh8a.v	$⊢ V = {Base}_{U}$
4		mapdh8a.s	$⊢ \underset{˙}{-} = -_{U}$
5		mapdh8a.o	$⊢ \underset{˙}{0} = 0_{U}$
6		mapdh8a.n	$⊢ N = LSpan (U)$
7		mapdh8a.c	$⊢ C = LCDual (K) (W)$
8		mapdh8a.d	$⊢ D = {Base}_{C}$
9		mapdh8a.r	$⊢ R = -_{C}$
10		mapdh8a.q	$⊢ Q = 0_{C}$
11		mapdh8a.j	$⊢ J = LSpan (C)$
12		mapdh8a.m	$⊢ M = mapd (K) (W)$
13		mapdh8a.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
14		mapdh8a.k	$⊢ φ \to (K \in HL \land W \in H)$
15		mapdh8e.f	$⊢ φ \to F \in D$
16		mapdh8e.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh8e.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
18		mapdh8e.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
19		mapdh8e.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
20		mapdh8e.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
21		mapdh8e.xy	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
22		mapdh8e.xt	$⊢ φ \to N (\{X\}) \neq N (\{T\})$
23		mapdh8e.yt	$⊢ φ \to N (\{Y\}) \neq N (\{T\})$
24		mapdh8e.e	$⊢ φ \to X \in N (\{Y, T\})$
25	18	eldifad	$⊢ φ \to X \in V$
26	19	eldifad	$⊢ φ \to Y \in V$
27	1 2 3 6 14 25 26	dvh3dim	$⊢ φ \to \exists w \in V \neg w \in N (\{X, Y\})$
28	14	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to (K \in HL \land W \in H)$
29	15	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to F \in D$
30	16	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to M (N (\{X\})) = J (\{F\})$
31	17	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to I (⟨X, F, Y⟩) = G$
32	18	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
33	19	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
34	20	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to T \in (V ∖ \{\underset{˙}{0}\})$
35	23	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{Y\}) \neq N (\{T\})$
36		eqid	$⊢ LSubSp (U) = LSubSp (U)$
37	1 2 14	dvhlmod	$⊢ φ \to U \in LMod$
38	37	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to U \in LMod$
39	3 36 6 37 25 26	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
40	39	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{X, Y\}) \in LSubSp (U)$
41		simp2	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to w \in V$
42		simp3	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to \neg w \in N (\{X, Y\})$
43	5 36 38 40 41 42	lssneln0	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to w \in (V ∖ \{\underset{˙}{0}\})$
44	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
45	20	eldifad	$⊢ φ \to T \in V$
46		prcom	$⊢ \{Y, T\} = \{T, Y\}$
47	46	fveq2i	$⊢ N (\{Y, T\}) = N (\{T, Y\})$
48	24 47	eleqtrdi	$⊢ φ \to X \in N (\{T, Y\})$
49	3 5 6 44 18 45 26 21 48	lspexch	$⊢ φ \to T \in N (\{X, Y\})$
50	36 6 37 39 49	ellspsn5	$⊢ φ \to N (\{T\}) \subseteq N (\{X, Y\})$
51	50	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{T\}) \subseteq N (\{X, Y\})$
52	37	adantr	$⊢ (φ \land w \in V) \to U \in LMod$
53	39	adantr	$⊢ (φ \land w \in V) \to N (\{X, Y\}) \in LSubSp (U)$
54		simpr	$⊢ (φ \land w \in V) \to w \in V$
55	3 36 6 52 53 54	ellspsn5b	$⊢ (φ \land w \in V) \to (w \in N (\{X, Y\}) \leftrightarrow N (\{w\}) \subseteq N (\{X, Y\}))$
56	55	biimprd	$⊢ (φ \land w \in V) \to (N (\{w\}) \subseteq N (\{X, Y\}) \to w \in N (\{X, Y\}))$
57	56	con3d	$⊢ (φ \land w \in V) \to (\neg w \in N (\{X, Y\}) \to \neg N (\{w\}) \subseteq N (\{X, Y\}))$
58	57	3impia	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to \neg N (\{w\}) \subseteq N (\{X, Y\})$
59		nssne2	$⊢ (N (\{T\}) \subseteq N (\{X, Y\}) \land \neg N (\{w\}) \subseteq N (\{X, Y\})) \to N (\{T\}) \neq N (\{w\})$
60	51 58 59	syl2anc	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{T\}) \neq N (\{w\})$
61	60	necomd	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{w\}) \neq N (\{T\})$
62	22	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{X\}) \neq N (\{T\})$
63	44	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to U \in LVec$
64	25	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to X \in V$
65	26	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to Y \in V$
66	3 6 63 41 64 65 42	lspindpi	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{Y\}))$
67	66	simprd	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{w\}) \neq N (\{Y\})$
68	67	necomd	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{Y\}) \neq N (\{w\})$
69	21	3ad2ant1	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to N (\{X\}) \neq N (\{Y\})$
70	3 5 6 63 32 65 41 69 42	lspindp2l	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to (N (\{Y\}) \neq N (\{w\}) \land \neg X \in N (\{Y, w\}))$
71	70	simprd	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to \neg X \in N (\{Y, w\})$
72	1 2 3 4 5 6 7 8 9 10 11 12 13 28 29 30 31 32 33 34 35 43 61 62 68 71	mapdh8d	$⊢ (φ \land w \in V \land \neg w \in N (\{X, Y\})) \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩)$
73	72	rexlimdv3a	$⊢ φ \to (\exists w \in V \neg w \in N (\{X, Y\}) \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩))$
74	27 73	mpd	$⊢ φ \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩)$

Metamath Proof Explorer

Theorem mapdh8e

Proof