mapdh9a

Description: Lemma for part (9) in Baer p. 48. TODO: why is this 50% larger than mapdh9aOLDN ? (Contributed by NM, 14-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)$
	mapdh8h.f	$⊢ φ \to F \in D$
	mapdh8h.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh9a.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh9a.t	$⊢ φ \to T \in V$
Assertion	mapdh9a	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), 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		mapdh8h.f	$⊢ φ \to F \in D$
16		mapdh8h.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh9a.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		mapdh9a.t	$⊢ φ \to T \in V$
19	14	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to (K \in HL \land W \in H)$
20	15	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to F \in D$
21	16	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to M (N (\{X\})) = J (\{F\})$
22	17	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to X \in (V ∖ \{\underset{˙}{0}\})$
23		simp3ll	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to z \in (V ∖ \{\underset{˙}{0}\})$
24		simp3rl	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to w \in (V ∖ \{\underset{˙}{0}\})$
25		simplrl	$⊢ ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to N (\{z\}) \neq N (\{X\})$
26	25	3ad2ant3	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to N (\{z\}) \neq N (\{X\})$
27	26	necomd	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to N (\{X\}) \neq N (\{z\})$
28		simprrl	$⊢ ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to N (\{w\}) \neq N (\{X\})$
29	28	3ad2ant3	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to N (\{w\}) \neq N (\{X\})$
30	29	necomd	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to N (\{X\}) \neq N (\{w\})$
31		simplrr	$⊢ ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to N (\{z\}) \neq N (\{T\})$
32	31	3ad2ant3	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to N (\{z\}) \neq N (\{T\})$
33		simprrr	$⊢ ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to N (\{w\}) \neq N (\{T\})$
34	33	3ad2ant3	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to N (\{w\}) \neq N (\{T\})$
35	18	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to T \in V$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 19 20 21 22 23 24 27 30 32 34 35	mapdh8	$⊢ (φ \land (z \in V \land w \in V) \land ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)$
37	36	3exp	$⊢ φ \to ((z \in V \land w \in V) \to (((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)))$
38	37	ralrimivv	$⊢ φ \to \forall z \in V \forall w \in V (((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩))$
39	17	eldifad	$⊢ φ \to X \in V$
40	1 2 3 6 14 39 18	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, T\})$
41		eqid	$⊢ LSubSp (U) = LSubSp (U)$
42	1 2 14	dvhlmod	$⊢ φ \to U \in LMod$
43	42	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to U \in LMod$
44	3 41 6 42 39 18	lspprcl	$⊢ φ \to N (\{X, T\}) \in LSubSp (U)$
45	44	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to N (\{X, T\}) \in LSubSp (U)$
46		simplr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to z \in V$
47		simpr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to \neg z \in N (\{X, T\})$
48	5 41 43 45 46 47	lssneln0	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to z \in (V ∖ \{\underset{˙}{0}\})$
49	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
50	49	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to U \in LVec$
51	39	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to X \in V$
52	18	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to T \in V$
53	3 6 50 46 51 52 47	lspindpi	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))$
54	48 53	jca	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))$
55	54	ex	$⊢ (φ \land z \in V) \to (\neg z \in N (\{X, T\}) \to (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))))$
56	55	reximdva	$⊢ φ \to (\exists z \in V \neg z \in N (\{X, T\}) \to \exists z \in V (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))))$
57	40 56	mpd	$⊢ φ \to \exists z \in V (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))$
58	14	ad2antrr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to (K \in HL \land W \in H)$
59	15	ad2antrr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to F \in D$
60	16	ad2antrr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to M (N (\{X\})) = J (\{F\})$
61	17	ad2antrr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to X \in (V ∖ \{\underset{˙}{0}\})$
62		simplr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to z \in V$
63		simprrl	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to N (\{z\}) \neq N (\{X\})$
64	63	necomd	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to N (\{X\}) \neq N (\{z\})$
65	10 13 1 12 2 3 4 5 6 7 8 9 11 58 59 60 61 62 64	mapdhcl	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to I (⟨X, F, z⟩) \in D$
66		eqidd	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to I (⟨X, F, z⟩) = I (⟨X, F, z⟩)$
67		simprl	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to z \in (V ∖ \{\underset{˙}{0}\})$
68	10 13 1 12 2 3 4 5 6 7 8 9 11 58 59 60 61 67 65 64	mapdheq	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to (I (⟨X, F, z⟩) = I (⟨X, F, z⟩) \leftrightarrow (M (N (\{z\})) = J (\{I (⟨X, F, z⟩)\}) \land M (N (\{X \underset{˙}{-} z\})) = J (\{F R I (⟨X, F, z⟩)\})))$
69	66 68	mpbid	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to (M (N (\{z\})) = J (\{I (⟨X, F, z⟩)\}) \land M (N (\{X \underset{˙}{-} z\})) = J (\{F R I (⟨X, F, z⟩)\}))$
70	69	simpld	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to M (N (\{z\})) = J (\{I (⟨X, F, z⟩)\})$
71	18	ad2antrr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to T \in V$
72		simprrr	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to N (\{z\}) \neq N (\{T\})$
73	10 13 1 12 2 3 4 5 6 7 8 9 11 58 65 70 67 71 72	mapdhcl	$⊢ ((φ \land z \in V) \land (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) \in D$
74	73	ex	$⊢ (φ \land z \in V) \to ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) \in D)$
75	74	ancld	$⊢ (φ \land z \in V) \to ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D))$
76	75	reximdva	$⊢ φ \to (\exists z \in V (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to \exists z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D))$
77	57 76	mpd	$⊢ φ \to \exists z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D)$
78		eleq1w	$⊢ z = w \to (z \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow w \in (V ∖ \{\underset{˙}{0}\}))$
79		sneq	$⊢ z = w \to \{z\} = \{w\}$
80	79	fveq2d	$⊢ z = w \to N (\{z\}) = N (\{w\})$
81	80	neeq1d	$⊢ z = w \to (N (\{z\}) \neq N (\{X\}) \leftrightarrow N (\{w\}) \neq N (\{X\}))$
82	80	neeq1d	$⊢ z = w \to (N (\{z\}) \neq N (\{T\}) \leftrightarrow N (\{w\}) \neq N (\{T\}))$
83	81 82	anbi12d	$⊢ z = w \to ((N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})) \leftrightarrow (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))$
84	78 83	anbi12d	$⊢ z = w \to ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \leftrightarrow (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))))$
85		oteq1	$⊢ z = w \to ⟨z, I (⟨X, F, z⟩), T⟩ = ⟨w, I (⟨X, F, z⟩), T⟩$
86		oteq3	$⊢ z = w \to ⟨X, F, z⟩ = ⟨X, F, w⟩$
87	86	fveq2d	$⊢ z = w \to I (⟨X, F, z⟩) = I (⟨X, F, w⟩)$
88	87	oteq2d	$⊢ z = w \to ⟨w, I (⟨X, F, z⟩), T⟩ = ⟨w, I (⟨X, F, w⟩), T⟩$
89	85 88	eqtrd	$⊢ z = w \to ⟨z, I (⟨X, F, z⟩), T⟩ = ⟨w, I (⟨X, F, w⟩), T⟩$
90	89	fveq2d	$⊢ z = w \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)$
91	84 90	reusv3	$⊢ \exists z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D) \to (\forall z \in V \forall w \in V (((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)) \leftrightarrow \exists y \in D \forall z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
92	77 91	syl	$⊢ φ \to (\forall z \in V \forall w \in V (((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \land (w \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\})))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)) \leftrightarrow \exists y \in D \forall z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
93	38 92	mpbid	$⊢ φ \to \exists y \in D \forall z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$
94		ioran	$⊢ \neg (z \in N (\{X\}) \lor z \in N (\{T\})) \leftrightarrow (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))$
95		elun	$⊢ z \in (N (\{X\}) \cup N (\{T\})) \leftrightarrow (z \in N (\{X\}) \lor z \in N (\{T\}))$
96	94 95	xchnxbir	$⊢ \neg z \in (N (\{X\}) \cup N (\{T\})) \leftrightarrow (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))$
97	42	ad2antrr	$⊢ ((φ \land z \in V) \land (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))) \to U \in LMod$
98	3 41 6	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
99	42 39 98	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
100	99	ad2antrr	$⊢ ((φ \land z \in V) \land (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))) \to N (\{X\}) \in LSubSp (U)$
101		simplr	$⊢ ((φ \land z \in V) \land (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))) \to z \in V$
102		simprl	$⊢ ((φ \land z \in V) \land (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))) \to \neg z \in N (\{X\})$
103	5 41 97 100 101 102	lssneln0	$⊢ ((φ \land z \in V) \land (\neg z \in N (\{X\}) \land \neg z \in N (\{T\}))) \to z \in (V ∖ \{\underset{˙}{0}\})$
104	103	ex	$⊢ (φ \land z \in V) \to ((\neg z \in N (\{X\}) \land \neg z \in N (\{T\})) \to z \in (V ∖ \{\underset{˙}{0}\}))$
105	42	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to U \in LMod$
106		simplr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to z \in V$
107	39	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to X \in V$
108		simpr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to \neg z \in N (\{X\})$
109	3 6 105 106 107 108	lspsnne2	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to N (\{z\}) \neq N (\{X\})$
110	109	ex	$⊢ (φ \land z \in V) \to (\neg z \in N (\{X\}) \to N (\{z\}) \neq N (\{X\}))$
111	42	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{T\})) \to U \in LMod$
112		simplr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{T\})) \to z \in V$
113	18	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{T\})) \to T \in V$
114		simpr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{T\})) \to \neg z \in N (\{T\})$
115	3 6 111 112 113 114	lspsnne2	$⊢ ((φ \land z \in V) \land \neg z \in N (\{T\})) \to N (\{z\}) \neq N (\{T\})$
116	115	ex	$⊢ (φ \land z \in V) \to (\neg z \in N (\{T\}) \to N (\{z\}) \neq N (\{T\}))$
117	110 116	anim12d	$⊢ (φ \land z \in V) \to ((\neg z \in N (\{X\}) \land \neg z \in N (\{T\})) \to (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\})))$
118	104 117	jcad	$⊢ (φ \land z \in V) \to ((\neg z \in N (\{X\}) \land \neg z \in N (\{T\})) \to (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))))$
119	96 118	syl5bi	$⊢ (φ \land z \in V) \to (\neg z \in (N (\{X\}) \cup N (\{T\})) \to (z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))))$
120	119	imim1d	$⊢ (φ \land z \in V) \to (((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \to (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
121	120	ralimdva	$⊢ φ \to (\forall z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \to \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
122	121	reximdv	$⊢ φ \to (\exists y \in D \forall z \in V ((z \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \to \exists y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
123	93 122	mpd	$⊢ φ \to \exists y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$
124	3 6 42 39 18	lspprid1	$⊢ φ \to X \in N (\{X, T\})$
125	41 6 42 44 124	lspsnel5a	$⊢ φ \to N (\{X\}) \subseteq N (\{X, T\})$
126	3 6 42 39 18	lspprid2	$⊢ φ \to T \in N (\{X, T\})$
127	41 6 42 44 126	lspsnel5a	$⊢ φ \to N (\{T\}) \subseteq N (\{X, T\})$
128	125 127	unssd	$⊢ φ \to N (\{X\}) \cup N (\{T\}) \subseteq N (\{X, T\})$
129	128	ssneld	$⊢ φ \to (\neg z \in N (\{X, T\}) \to \neg z \in (N (\{X\}) \cup N (\{T\})))$
130	129	reximdv	$⊢ φ \to (\exists z \in V \neg z \in N (\{X, T\}) \to \exists z \in V \neg z \in (N (\{X\}) \cup N (\{T\})))$
131	40 130	mpd	$⊢ φ \to \exists z \in V \neg z \in (N (\{X\}) \cup N (\{T\}))$
132		reusv1	$⊢ \exists z \in V \neg z \in (N (\{X\}) \cup N (\{T\})) \to (\exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow \exists y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
133	131 132	syl	$⊢ φ \to (\exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow \exists y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
134	123 133	mpbird	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$

Metamath Proof Explorer

Theorem mapdh9a

Proof