mapdh8ad

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 13-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)$
	mapdh8ac.f	$⊢ φ \to F \in D$
	mapdh8ac.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh8ac.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh8ac.ee	$⊢ φ \to I (⟨X, F, Z⟩) = E$
	mapdh8ac.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ac.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ac.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ac.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ac.yn	$⊢ φ \to N (\{X\}) = N (\{T\})$
	mapdh8ad.xy	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdh8ad.xz	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
Assertion	mapdh8ad	$⊢ φ \to I (⟨Y, G, T⟩) = I (⟨Z, E, 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		mapdh8ac.f	$⊢ φ \to F \in D$
16		mapdh8ac.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh8ac.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
18		mapdh8ac.ee	$⊢ φ \to I (⟨X, F, Z⟩) = E$
19		mapdh8ac.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
20		mapdh8ac.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
21		mapdh8ac.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
22		mapdh8ac.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
23		mapdh8ac.yn	$⊢ φ \to N (\{X\}) = N (\{T\})$
24		mapdh8ad.xy	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
25		mapdh8ad.xz	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
26	19	eldifad	$⊢ φ \to X \in V$
27	20	eldifad	$⊢ φ \to Y \in V$
28	21	eldifad	$⊢ φ \to Z \in V$
29	1 2 3 6 14 26 27 28	dvh3dim2	$⊢ φ \to \exists w \in V (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))$
30	14	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to (K \in HL \land W \in H)$
31	15	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to F \in D$
32	16	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to M (N (\{X\})) = J (\{F\})$
33	17	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to I (⟨X, F, Y⟩) = G$
34	18	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to I (⟨X, F, Z⟩) = E$
35	19	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to X \in (V ∖ \{\underset{˙}{0}\})$
36	20	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to Y \in (V ∖ \{\underset{˙}{0}\})$
37	21	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to Z \in (V ∖ \{\underset{˙}{0}\})$
38	22	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to T \in (V ∖ \{\underset{˙}{0}\})$
39	23	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to N (\{X\}) = N (\{T\})$
40		eqidd	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to I (⟨X, F, w⟩) = I (⟨X, F, w⟩)$
41		eqid	$⊢ LSubSp (U) = LSubSp (U)$
42	1 2 14	dvhlmod	$⊢ φ \to U \in LMod$
43	42	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to U \in LMod$
44	3 41 6 42 26 27	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
45	44	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to N (\{X, Y\}) \in LSubSp (U)$
46		simp2	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to w \in V$
47		simp3l	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to \neg w \in N (\{X, Y\})$
48	5 41 43 45 46 47	lssneln0	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to w \in (V ∖ \{\underset{˙}{0}\})$
49	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
50	49	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to U \in LVec$
51	26	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to X \in V$
52	27	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to Y \in V$
53	3 6 50 46 51 52 47	lspindpi	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{Y\}))$
54	53	simprd	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to N (\{w\}) \neq N (\{Y\})$
55	54	necomd	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to N (\{Y\}) \neq N (\{w\})$
56		simpl1	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to φ$
57	56 49	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to U \in LVec$
58	56 19	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
59		simpl2	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to w \in V$
60	56 27	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to Y \in V$
61	56 24	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to N (\{X\}) \neq N (\{Y\})$
62		simpr	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to X \in N (\{Y, w\})$
63		prcom	$⊢ \{Y, w\} = \{w, Y\}$
64	63	fveq2i	$⊢ N (\{Y, w\}) = N (\{w, Y\})$
65	62 64	eleqtrdi	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to X \in N (\{w, Y\})$
66	3 5 6 57 58 59 60 61 65	lspexch	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{Y, w\})) \to w \in N (\{X, Y\})$
67	47 66	mtand	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to \neg X \in N (\{Y, w\})$
68	28	3ad2ant1	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to Z \in V$
69		simp3r	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to \neg w \in N (\{X, Z\})$
70	3 6 50 46 51 68 69	lspindpi	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{Z\}))$
71	70	simprd	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to N (\{w\}) \neq N (\{Z\})$
72		simpl1	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to φ$
73	72 49	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to U \in LVec$
74	72 19	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
75		simpl2	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to w \in V$
76	72 28	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to Z \in V$
77	72 25	syl	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to N (\{X\}) \neq N (\{Z\})$
78		simpr	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to X \in N (\{w, Z\})$
79	3 5 6 73 74 75 76 77 78	lspexch	$⊢ ((φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \land X \in N (\{w, Z\})) \to w \in N (\{X, Z\})$
80	69 79	mtand	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to \neg X \in N (\{w, Z\})$
81	1 2 3 4 5 6 7 8 9 10 11 12 13 30 31 32 33 34 35 36 37 38 39 40 48 55 67 71 80	mapdh8ac	$⊢ (φ \land w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\}))) \to I (⟨Y, G, T⟩) = I (⟨Z, E, T⟩)$
82	81	rexlimdv3a	$⊢ φ \to (\exists w \in V (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{X, Z\})) \to I (⟨Y, G, T⟩) = I (⟨Z, E, T⟩))$
83	29 82	mpd	$⊢ φ \to I (⟨Y, G, T⟩) = I (⟨Z, E, T⟩)$

Metamath Proof Explorer

Theorem mapdh8ad

Proof