mapdh9aOLDN

Description: Lemma for part (9) in Baer p. 48. (Contributed by NM, 14-May-2015) (New usage is discouraged.)

	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	mapdh9aOLDN	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in N (\{X, 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 (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to (K \in HL \land W \in H)$
20	15	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to F \in D$
21	16	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to M (N (\{X\})) = J (\{F\})$
22	17	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to X \in (V ∖ \{\underset{˙}{0}\})$
23		eqid	$⊢ LSubSp (U) = LSubSp (U)$
24	1 2 14	dvhlmod	$⊢ φ \to U \in LMod$
25	24	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to U \in LMod$
26	17	eldifad	$⊢ φ \to X \in V$
27	3 23 6 24 26 18	lspprcl	$⊢ φ \to N (\{X, T\}) \in LSubSp (U)$
28	27	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{X, T\}) \in LSubSp (U)$
29		simp2l	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to z \in V$
30		simp3l	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to \neg z \in N (\{X, T\})$
31	5 23 25 28 29 30	lssneln0	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to z \in (V ∖ \{\underset{˙}{0}\})$
32		simp2r	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to w \in V$
33		simp3r	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to \neg w \in N (\{X, T\})$
34	5 23 25 28 32 33	lssneln0	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to w \in (V ∖ \{\underset{˙}{0}\})$
35	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
36	35	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to U \in LVec$
37	26	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to X \in V$
38	18	3ad2ant1	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to T \in V$
39	3 6 36 29 37 38 30	lspindpi	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))$
40	39	simpld	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{z\}) \neq N (\{X\})$
41	40	necomd	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{X\}) \neq N (\{z\})$
42	3 6 36 32 37 38 33	lspindpi	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{T\}))$
43	42	simpld	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{w\}) \neq N (\{X\})$
44	43	necomd	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{X\}) \neq N (\{w\})$
45	39	simprd	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{z\}) \neq N (\{T\})$
46	42	simprd	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to N (\{w\}) \neq N (\{T\})$
47	1 2 3 4 5 6 7 8 9 10 11 12 13 19 20 21 22 31 34 41 44 45 46 38	mapdh8	$⊢ (φ \land (z \in V \land w \in V) \land (\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\}))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)$
48	47	3exp	$⊢ φ \to ((z \in V \land w \in V) \to ((\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\})) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)))$
49	48	ralrimivv	$⊢ φ \to \forall z \in V \forall w \in V ((\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, T\})) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩))$
50	1 2 3 6 14 26 18	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, T\})$
51	14	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to (K \in HL \land W \in H)$
52	15	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to F \in D$
53	16	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to M (N (\{X\})) = J (\{F\})$
54	17	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
55		simplr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to z \in V$
56	35	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to U \in LVec$
57	26	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to X \in V$
58	18	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to T \in V$
59		simpr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to \neg z \in N (\{X, T\})$
60	3 6 56 55 57 58 59	lspindpi	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{T\}))$
61	60	simpld	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to N (\{z\}) \neq N (\{X\})$
62	61	necomd	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to N (\{X\}) \neq N (\{z\})$
63	10 13 1 12 2 3 4 5 6 7 8 9 11 51 52 53 54 55 62	mapdhcl	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to I (⟨X, F, z⟩) \in D$
64		eqidd	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to I (⟨X, F, z⟩) = I (⟨X, F, z⟩)$
65	24	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to U \in LMod$
66	27	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to N (\{X, T\}) \in LSubSp (U)$
67	5 23 65 66 55 59	lssneln0	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to z \in (V ∖ \{\underset{˙}{0}\})$
68	10 13 1 12 2 3 4 5 6 7 8 9 11 51 52 53 54 67 63 62	mapdheq	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, 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	64 68	mpbid	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, 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 \neg z \in N (\{X, T\})) \to M (N (\{z\})) = J (\{I (⟨X, F, z⟩)\})$
71	60	simprd	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to N (\{z\}) \neq N (\{T\})$
72	10 13 1 12 2 3 4 5 6 7 8 9 11 51 63 70 67 58 71	mapdhcl	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X, T\})) \to I (⟨z, I (⟨X, F, z⟩), T⟩) \in D$
73	72	ex	$⊢ (φ \land z \in V) \to (\neg z \in N (\{X, T\}) \to I (⟨z, I (⟨X, F, z⟩), T⟩) \in D)$
74	73	ancld	$⊢ (φ \land z \in V) \to (\neg z \in N (\{X, T\}) \to (\neg z \in N (\{X, T\}) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D))$
75	74	reximdva	$⊢ φ \to (\exists z \in V \neg z \in N (\{X, T\}) \to \exists z \in V (\neg z \in N (\{X, T\}) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D))$
76	50 75	mpd	$⊢ φ \to \exists z \in V (\neg z \in N (\{X, T\}) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D)$
77		eleq1w	$⊢ z = w \to (z \in N (\{X, T\}) \leftrightarrow w \in N (\{X, T\}))$
78	77	notbid	$⊢ z = w \to (\neg z \in N (\{X, T\}) \leftrightarrow \neg w \in N (\{X, T\}))$
79		oteq1	$⊢ z = w \to ⟨z, I (⟨X, F, z⟩), T⟩ = ⟨w, I (⟨X, F, z⟩), T⟩$
80		oteq3	$⊢ z = w \to ⟨X, F, z⟩ = ⟨X, F, w⟩$
81	80	fveq2d	$⊢ z = w \to I (⟨X, F, z⟩) = I (⟨X, F, w⟩)$
82	81	oteq2d	$⊢ z = w \to ⟨w, I (⟨X, F, z⟩), T⟩ = ⟨w, I (⟨X, F, w⟩), T⟩$
83	79 82	eqtrd	$⊢ z = w \to ⟨z, I (⟨X, F, z⟩), T⟩ = ⟨w, I (⟨X, F, w⟩), T⟩$
84	83	fveq2d	$⊢ z = w \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨w, I (⟨X, F, w⟩), T⟩)$
85	78 84	reusv3	$⊢ \exists z \in V (\neg z \in N (\{X, T\}) \land I (⟨z, I (⟨X, F, z⟩), T⟩) \in D) \to (\forall z \in V \forall w \in V ((\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, 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 (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
86	76 85	syl	$⊢ φ \to (\forall z \in V \forall w \in V ((\neg z \in N (\{X, T\}) \land \neg w \in N (\{X, 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 (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
87	49 86	mpbid	$⊢ φ \to \exists y \in D \forall z \in V (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$
88		reusv1	$⊢ \exists z \in V \neg z \in N (\{X, T\}) \to (\exists! y \in D \forall z \in V (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow \exists y \in D \forall z \in V (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
89	50 88	syl	$⊢ φ \to (\exists! y \in D \forall z \in V (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow \exists y \in D \forall z \in V (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)))$
90	87 89	mpbird	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in N (\{X, T\}) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$

Metamath Proof Explorer

Theorem mapdh9aOLDN

Proof