hdmap1eulem

Description: Lemma for hdmap1eu . TODO: combine with hdmap1eu or at least share some hypotheses. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1eulem.h	$⊢ H = LHyp (K)$
	hdmap1eulem.u	$⊢ U = DVecH (K) (W)$
	hdmap1eulem.v	$⊢ V = {Base}_{U}$
	hdmap1eulem.s	$⊢ \underset{˙}{-} = -_{U}$
	hdmap1eulem.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap1eulem.n	$⊢ N = LSpan (U)$
	hdmap1eulem.c	$⊢ C = LCDual (K) (W)$
	hdmap1eulem.d	$⊢ D = {Base}_{C}$
	hdmap1eulem.r	$⊢ R = -_{C}$
	hdmap1eulem.q	$⊢ Q = 0_{C}$
	hdmap1eulem.j	$⊢ J = LSpan (C)$
	hdmap1eulem.m	$⊢ M = mapd (K) (W)$
	hdmap1eulem.i	$⊢ I = HDMap1 (K) (W)$
	hdmap1eulem.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap1eulem.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	hdmap1eulem.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1eulem.f	$⊢ φ \to F \in D$
	hdmap1eulem.y	$⊢ φ \to T \in V$
	hdmap1eulem.l	$⊢ L = (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\})))))$
Assertion	hdmap1eulem	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$

Proof

Step	Hyp	Ref	Expression
1		hdmap1eulem.h	$⊢ H = LHyp (K)$
2		hdmap1eulem.u	$⊢ U = DVecH (K) (W)$
3		hdmap1eulem.v	$⊢ V = {Base}_{U}$
4		hdmap1eulem.s	$⊢ \underset{˙}{-} = -_{U}$
5		hdmap1eulem.o	$⊢ \underset{˙}{0} = 0_{U}$
6		hdmap1eulem.n	$⊢ N = LSpan (U)$
7		hdmap1eulem.c	$⊢ C = LCDual (K) (W)$
8		hdmap1eulem.d	$⊢ D = {Base}_{C}$
9		hdmap1eulem.r	$⊢ R = -_{C}$
10		hdmap1eulem.q	$⊢ Q = 0_{C}$
11		hdmap1eulem.j	$⊢ J = LSpan (C)$
12		hdmap1eulem.m	$⊢ M = mapd (K) (W)$
13		hdmap1eulem.i	$⊢ I = HDMap1 (K) (W)$
14		hdmap1eulem.k	$⊢ φ \to (K \in HL \land W \in H)$
15		hdmap1eulem.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
16		hdmap1eulem.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
17		hdmap1eulem.f	$⊢ φ \to F \in D$
18		hdmap1eulem.y	$⊢ φ \to T \in V$
19		hdmap1eulem.l	$⊢ L = (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\})))))$
20	1 2 3 4 5 6 7 8 9 10 11 12 19 14 17 15 16 18	mapdh9a	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = L (⟨z, L (⟨X, F, z⟩), T⟩))$
21	14	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to (K \in HL \land W \in H)$
22	16	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to X \in (V ∖ \{\underset{˙}{0}\})$
23	17	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to F \in D$
24		simplr	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to z \in V$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 21 22 23 24 19	hdmap1valc	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to I (⟨X, F, z⟩) = L (⟨X, F, z⟩)$
26	25	oteq2d	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to ⟨z, I (⟨X, F, z⟩), T⟩ = ⟨z, L (⟨X, F, z⟩), T⟩$
27	26	fveq2d	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = I (⟨z, L (⟨X, F, z⟩), T⟩)$
28		elun1	$⊢ z \in N (\{X\}) \to z \in (N (\{X\}) \cup N (\{T\}))$
29	28	con3i	$⊢ \neg z \in (N (\{X\}) \cup N (\{T\})) \to \neg z \in N (\{X\})$
30	14	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to (K \in HL \land W \in H)$
31		eqid	$⊢ LSubSp (U) = LSubSp (U)$
32	1 2 14	dvhlmod	$⊢ φ \to U \in LMod$
33	32	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to U \in LMod$
34	16	eldifad	$⊢ φ \to X \in V$
35	34	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to X \in V$
36	3 31 6	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
37	33 35 36	syl2anc	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to N (\{X\}) \in LSubSp (U)$
38		simplr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to z \in V$
39		simpr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to \neg z \in N (\{X\})$
40	5 31 33 37 38 39	lssneln0	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to z \in (V ∖ \{\underset{˙}{0}\})$
41	17	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to F \in D$
42	15	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to M (N (\{X\})) = J (\{F\})$
43	16	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
44	3 6 33 38 35 39	lspsnne2	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to N (\{z\}) \neq N (\{X\})$
45	44	necomd	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to N (\{X\}) \neq N (\{z\})$
46	10 19 1 12 2 3 4 5 6 7 8 9 11 30 41 42 43 38 45	mapdhcl	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to L (⟨X, F, z⟩) \in D$
47	18	ad2antrr	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to T \in V$
48	1 2 3 4 5 6 7 8 9 10 11 12 13 30 40 46 47 19	hdmap1valc	$⊢ ((φ \land z \in V) \land \neg z \in N (\{X\})) \to I (⟨z, L (⟨X, F, z⟩), T⟩) = L (⟨z, L (⟨X, F, z⟩), T⟩)$
49	29 48	sylan2	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to I (⟨z, L (⟨X, F, z⟩), T⟩) = L (⟨z, L (⟨X, F, z⟩), T⟩)$
50	27 49	eqtrd	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to I (⟨z, I (⟨X, F, z⟩), T⟩) = L (⟨z, L (⟨X, F, z⟩), T⟩)$
51	50	eqeq2d	$⊢ ((φ \land z \in V) \land \neg z \in (N (\{X\}) \cup N (\{T\}))) \to (y = I (⟨z, I (⟨X, F, z⟩), T⟩) \leftrightarrow y = L (⟨z, L (⟨X, F, z⟩), T⟩))$
52	51	pm5.74da	$⊢ (φ \land z \in V) \to ((\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = L (⟨z, L (⟨X, F, z⟩), T⟩)))$
53	52	ralbidva	$⊢ φ \to (\forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = L (⟨z, L (⟨X, F, z⟩), T⟩)))$
54	53	reubidv	$⊢ φ \to (\exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩)) \leftrightarrow \exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = L (⟨z, L (⟨X, F, z⟩), T⟩)))$
55	20 54	mpbird	$⊢ φ \to \exists! y \in D \forall z \in V (\neg z \in (N (\{X\}) \cup N (\{T\})) \to y = I (⟨z, I (⟨X, F, z⟩), T⟩))$

Metamath Proof Explorer

Theorem hdmap1eulem

Proof