mapdh8ab

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)$
	mapdh8ab.f	$⊢ φ \to F \in D$
	mapdh8ab.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh8ab.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh8ab.ee	$⊢ φ \to I (⟨X, F, Z⟩) = E$
	mapdh8ab.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ab.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ab.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ab.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8ab.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
	mapdh8ab.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	mapdh8ab.yn	$⊢ φ \to N (\{X\}) = N (\{T\})$
Assertion	mapdh8ab	$⊢ φ \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		mapdh8ab.f	$⊢ φ \to F \in D$
16		mapdh8ab.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh8ab.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
18		mapdh8ab.ee	$⊢ φ \to I (⟨X, F, Z⟩) = E$
19		mapdh8ab.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
20		mapdh8ab.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
21		mapdh8ab.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
22		mapdh8ab.t	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
23		mapdh8ab.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
24		mapdh8ab.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
25		mapdh8ab.yn	$⊢ φ \to N (\{X\}) = N (\{T\})$
26	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
27	19	eldifad	$⊢ φ \to X \in V$
28	20	eldifad	$⊢ φ \to Y \in V$
29	21	eldifad	$⊢ φ \to Z \in V$
30	3 6 26 27 28 29 24	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$
31	30	simprd	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
32	31	necomd	$⊢ φ \to N (\{Z\}) \neq N (\{X\})$
33	32 25	neeqtrd	$⊢ φ \to N (\{Z\}) \neq N (\{T\})$
34	25	sseq1d	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y, Z\}) \leftrightarrow N (\{T\}) \subseteq N (\{Y, Z\}))$
35		eqid	$⊢ LSubSp (U) = LSubSp (U)$
36	1 2 14	dvhlmod	$⊢ φ \to U \in LMod$
37	3 35 6 36 28 29	lspprcl	$⊢ φ \to N (\{Y, Z\}) \in LSubSp (U)$
38	3 35 6 36 37 27	ellspsn5b	$⊢ φ \to (X \in N (\{Y, Z\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y, Z\}))$
39	22	eldifad	$⊢ φ \to T \in V$
40	3 35 6 36 37 39	ellspsn5b	$⊢ φ \to (T \in N (\{Y, Z\}) \leftrightarrow N (\{T\}) \subseteq N (\{Y, Z\}))$
41	34 38 40	3bitr4d	$⊢ φ \to (X \in N (\{Y, Z\}) \leftrightarrow T \in N (\{Y, Z\}))$
42	24 41	mtbid	$⊢ φ \to \neg T \in N (\{Y, Z\})$
43	26	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to U \in LVec$
44	20	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
45	39	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to T \in V$
46	29	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to Z \in V$
47	23	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to N (\{Y\}) \neq N (\{Z\})$
48		simpr	$⊢ (φ \land Y \in N (\{Z, T\})) \to Y \in N (\{Z, T\})$
49		prcom	$⊢ \{Z, T\} = \{T, Z\}$
50	49	fveq2i	$⊢ N (\{Z, T\}) = N (\{T, Z\})$
51	48 50	eleqtrdi	$⊢ (φ \land Y \in N (\{Z, T\})) \to Y \in N (\{T, Z\})$
52	3 5 6 43 44 45 46 47 51	lspexch	$⊢ (φ \land Y \in N (\{Z, T\})) \to T \in N (\{Y, Z\})$
53	42 52	mtand	$⊢ φ \to \neg Y \in N (\{Z, T\})$
54	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 33 22 53 24	mapdh8aa	$⊢ φ \to I (⟨Y, G, T⟩) = I (⟨Z, E, T⟩)$

Metamath Proof Explorer

Theorem mapdh8ab

Proof