mapdheq4

Description: Lemma for ~? mapdh . Part (4) in Baer p. 46. (Contributed by NM, 12-Apr-2015)

	Ref	Expression
Hypotheses	mapdh.q	$⊢ Q = 0_{C}$
	mapdh.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\})))))$
	mapdh.h	$⊢ H = LHyp (K)$
	mapdh.m	$⊢ M = mapd (K) (W)$
	mapdh.u	$⊢ U = DVecH (K) (W)$
	mapdh.v	$⊢ V = {Base}_{U}$
	mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdh.n	$⊢ N = LSpan (U)$
	mapdh.c	$⊢ C = LCDual (K) (W)$
	mapdh.d	$⊢ D = {Base}_{C}$
	mapdh.r	$⊢ R = -_{C}$
	mapdh.j	$⊢ J = LSpan (C)$
	mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdhc.f	$⊢ φ \to F \in D$
	mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdhe4.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdhe.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdh.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	mapdh.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
	mapdh.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh.ee	$⊢ φ \to I (⟨X, F, Z⟩) = E$
Assertion	mapdheq4	$⊢ φ \to I (⟨Y, G, Z⟩) = E$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$⊢ Q = 0_{C}$
2		mapdh.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\})))))$
3		mapdh.h	$⊢ H = LHyp (K)$
4		mapdh.m	$⊢ M = mapd (K) (W)$
5		mapdh.u	$⊢ U = DVecH (K) (W)$
6		mapdh.v	$⊢ V = {Base}_{U}$
7		mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
8		mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
9		mapdh.n	$⊢ N = LSpan (U)$
10		mapdh.c	$⊢ C = LCDual (K) (W)$
11		mapdh.d	$⊢ D = {Base}_{C}$
12		mapdh.r	$⊢ R = -_{C}$
13		mapdh.j	$⊢ J = LSpan (C)$
14		mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
15		mapdhc.f	$⊢ φ \to F \in D$
16		mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		mapdhe4.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
19		mapdhe.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
20		mapdh.xn	$⊢ φ \to \neg X \in N (\{Y, Z\})$
21		mapdh.yz	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
22		mapdh.eg	$⊢ φ \to I (⟨X, F, Y⟩) = G$
23		mapdh.ee	$⊢ φ \to I (⟨X, F, Z⟩) = E$
24	19	eldifad	$⊢ φ \to Z \in V$
25	3 5 14	dvhlvec	$⊢ φ \to U \in LVec$
26	17	eldifad	$⊢ φ \to X \in V$
27	6 8 9 25 18 24 26 21 20	lspindp1	$⊢ φ \to (N (\{X\}) \neq N (\{Z\}) \land \neg Y \in N (\{X, Z\}))$
28	27	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 24 28	mapdhcl	$⊢ φ \to I (⟨X, F, Z⟩) \in D$
30	23 29	eqeltrrd	$⊢ φ \to E \in D$
31	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 19 30 28	mapdheq	$⊢ φ \to (I (⟨X, F, Z⟩) = E \leftrightarrow (M (N (\{Z\})) = J (\{E\}) \land M (N (\{X \underset{˙}{-} Z\})) = J (\{F R E\})))$
32	23 31	mpbid	$⊢ φ \to (M (N (\{Z\})) = J (\{E\}) \land M (N (\{X \underset{˙}{-} Z\})) = J (\{F R E\}))$
33	32	simpld	$⊢ φ \to M (N (\{Z\})) = J (\{E\})$
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	mapdheq4lem	$⊢ φ \to M (N (\{Y \underset{˙}{-} Z\})) = J (\{G R E\})$
35	18	eldifad	$⊢ φ \to Y \in V$
36	6 8 9 25 35 19 26 21 20	lspindp2	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land \neg Z \in N (\{X, Y\}))$
37	36	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 35 37	mapdhcl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
39	22 38	eqeltrrd	$⊢ φ \to G \in D$
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 39 37	mapdheq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})))$
41	22 40	mpbid	$⊢ φ \to (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))$
42	41	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
43	1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 42 18 19 30 21	mapdheq	$⊢ φ \to (I (⟨Y, G, Z⟩) = E \leftrightarrow (M (N (\{Z\})) = J (\{E\}) \land M (N (\{Y \underset{˙}{-} Z\})) = J (\{G R E\})))$
44	33 34 43	mpbir2and	$⊢ φ \to I (⟨Y, G, Z⟩) = E$

Metamath Proof Explorer

Theorem mapdheq4

Proof