mapdh8d

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 6-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)$
	mapdh8d.f	$⊢ φ \to F \in D$
	mapdh8d.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh8b.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh8d.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8d.xt	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8d.yz	$⊢ φ \to N (\{Y\}) \neq N (\{T\})$
	mapdh8d.w	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8d.wt	$⊢ φ \to N (\{w\}) \neq N (\{T\})$
	mapdh8d.ut	$⊢ φ \to N (\{X\}) \neq N (\{T\})$
	mapdh8d.vw	$⊢ φ \to N (\{Y\}) \neq N (\{w\})$
	mapdh8d.xn	$⊢ φ \to \neg X \in N (\{Y, w\})$
Assertion	mapdh8d	$⊢ φ \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		mapdh8d.f	$⊢ φ \to F \in D$
16		mapdh8d.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh8b.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
18		mapdh8d.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
19		mapdh8d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
20		mapdh8d.xt	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
21		mapdh8d.yz	$⊢ φ \to N (\{Y\}) \neq N (\{T\})$
22		mapdh8d.w	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
23		mapdh8d.wt	$⊢ φ \to N (\{w\}) \neq N (\{T\})$
24		mapdh8d.ut	$⊢ φ \to N (\{X\}) \neq N (\{T\})$
25		mapdh8d.vw	$⊢ φ \to N (\{Y\}) \neq N (\{w\})$
26		mapdh8d.xn	$⊢ φ \to \neg X \in N (\{Y, w\})$
27	14	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to (K \in HL \land W \in H)$
28	19	eldifad	$⊢ φ \to Y \in V$
29	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
30	18	eldifad	$⊢ φ \to X \in V$
31	22	eldifad	$⊢ φ \to w \in V$
32	3 6 29 30 28 31 26	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{w\}))$
33	32	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
34	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 18 28 33	mapdhcl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
35	17 34	eqeltrrd	$⊢ φ \to G \in D$
36	35	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to G \in D$
37	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 18 19 35 33	mapdheq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})))$
38	17 37	mpbid	$⊢ φ \to (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))$
39	38	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
40	39	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to M (N (\{Y\})) = J (\{G\})$
41	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 25 22 26	mapdh8a	$⊢ φ \to I (⟨Y, G, w⟩) = I (⟨X, F, w⟩)$
42	41	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to I (⟨Y, G, w⟩) = I (⟨X, F, w⟩)$
43	19	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
44	22	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to w \in (V ∖ \{\underset{˙}{0}\})$
45	23	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to N (\{w\}) \neq N (\{T\})$
46	20	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to T \in (V ∖ \{\underset{˙}{0}\})$
47	25	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to N (\{Y\}) \neq N (\{w\})$
48		simpr	$⊢ (φ \land X \in N (\{Y, T\})) \to X \in N (\{Y, T\})$
49	26	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to \neg X \in N (\{Y, w\})$
50	1 2 3 4 5 6 7 8 9 10 11 12 13 27 36 40 42 43 44 45 46 47 48 49	mapdh8b	$⊢ (φ \land X \in N (\{Y, T\})) \to I (⟨w, I (⟨X, F, w⟩), T⟩) = I (⟨Y, G, T⟩)$
51	15	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to F \in D$
52	16	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to M (N (\{X\})) = J (\{F\})$
53		eqidd	$⊢ (φ \land X \in N (\{Y, T\})) \to I (⟨X, F, w⟩) = I (⟨X, F, w⟩)$
54	18	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
55	21	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to N (\{Y\}) \neq N (\{T\})$
56	24	adantr	$⊢ (φ \land X \in N (\{Y, T\})) \to N (\{X\}) \neq N (\{T\})$
57	1 2 3 4 5 6 7 8 9 10 11 12 13 27 51 52 53 54 43 46 55 44 45 56 47 48 49	mapdh8c	$⊢ (φ \land X \in N (\{Y, T\})) \to I (⟨w, I (⟨X, F, w⟩), T⟩) = I (⟨X, F, T⟩)$
58	50 57	eqtr3d	$⊢ (φ \land X \in N (\{Y, T\})) \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩)$
59	14	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to (K \in HL \land W \in H)$
60	15	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to F \in D$
61	16	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to M (N (\{X\})) = J (\{F\})$
62	17	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to I (⟨X, F, Y⟩) = G$
63	18	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
64	19	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
65	21	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to N (\{Y\}) \neq N (\{T\})$
66	20	adantr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to T \in (V ∖ \{\underset{˙}{0}\})$
67		simpr	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to \neg X \in N (\{Y, T\})$
68	1 2 3 4 5 6 7 8 9 10 11 12 13 59 60 61 62 63 64 65 66 67	mapdh8a	$⊢ (φ \land \neg X \in N (\{Y, T\})) \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩)$
69	58 68	pm2.61dan	$⊢ φ \to I (⟨Y, G, T⟩) = I (⟨X, F, T⟩)$

Metamath Proof Explorer

Theorem mapdh8d

Proof