mapdhcl

	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}\})$
	mapdhc.y	$⊢ φ \to Y \in V$
	mapdh.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
Assertion	mapdhcl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$

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		mapdhc.y	$⊢ φ \to Y \in V$
19		mapdh.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
20		oteq3	$⊢ Y = \underset{˙}{0} \to ⟨X, F, Y⟩ = ⟨X, F, \underset{˙}{0}⟩$
21	20	fveq2d	$⊢ Y = \underset{˙}{0} \to I (⟨X, F, Y⟩) = I (⟨X, F, \underset{˙}{0}⟩)$
22	21	eleq1d	$⊢ Y = \underset{˙}{0} \to (I (⟨X, F, Y⟩) \in D \leftrightarrow I (⟨X, F, \underset{˙}{0}⟩) \in D)$
23	17	adantr	$⊢ (φ \land Y \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
24	15	adantr	$⊢ (φ \land Y \neq \underset{˙}{0}) \to F \in D$
25	18	anim1i	$⊢ (φ \land Y \neq \underset{˙}{0}) \to (Y \in V \land Y \neq \underset{˙}{0})$
26		eldifsn	$⊢ Y \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in V \land Y \neq \underset{˙}{0})$
27	25 26	sylibr	$⊢ (φ \land Y \neq \underset{˙}{0}) \to Y \in (V ∖ \{\underset{˙}{0}\})$
28	1 2 23 24 27	mapdhval2	$⊢ (φ \land Y \neq \underset{˙}{0}) \to I (⟨X, F, Y⟩) = (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\})))$
29	14	adantr	$⊢ (φ \land Y \neq \underset{˙}{0}) \to (K \in HL \land W \in H)$
30	19	adantr	$⊢ (φ \land Y \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y\})$
31	16	adantr	$⊢ (φ \land Y \neq \underset{˙}{0}) \to M (N (\{X\})) = J (\{F\})$
32	3 4 5 6 7 8 9 10 11 12 13 29 23 27 24 30 31	mapdpg	$⊢ (φ \land Y \neq \underset{˙}{0}) \to \exists! h \in D (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))$
33		riotacl	$⊢ \exists! h \in D (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\})) \to (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))) \in D$
34	32 33	syl	$⊢ (φ \land Y \neq \underset{˙}{0}) \to (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))) \in D$
35	28 34	eqeltrd	$⊢ (φ \land Y \neq \underset{˙}{0}) \to I (⟨X, F, Y⟩) \in D$
36	1 2 8 17 15	mapdhval0	$⊢ φ \to I (⟨X, F, \underset{˙}{0}⟩) = Q$
37	3 10 11 1 14	lcd0vcl	$⊢ φ \to Q \in D$
38	36 37	eqeltrd	$⊢ φ \to I (⟨X, F, \underset{˙}{0}⟩) \in D$
39	22 35 38	pm2.61ne	$⊢ φ \to I (⟨X, F, Y⟩) \in D$

Metamath Proof Explorer

Theorem mapdhcl

Proof