hdmapval2

Description: Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two =/= hypothesis? Consider hdmaplem1 through hdmaplem4 , which would become obsolete. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmapval2.h	$⊢ H = LHyp (K)$
	hdmapval2.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapval2.u	$⊢ U = DVecH (K) (W)$
	hdmapval2.v	$⊢ V = {Base}_{U}$
	hdmapval2.n	$⊢ N = LSpan (U)$
	hdmapval2.c	$⊢ C = LCDual (K) (W)$
	hdmapval2.d	$⊢ D = {Base}_{C}$
	hdmapval2.j	$⊢ J = HVMap (K) (W)$
	hdmapval2.i	$⊢ I = HDMap1 (K) (W)$
	hdmapval2.s	$⊢ S = HDMap (K) (W)$
	hdmapval2.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapval2.t	$⊢ φ \to T \in V$
	hdmapval2.x	$⊢ φ \to X \in V$
	hdmapval2.ne	$⊢ φ \to \neg X \in (N (\{E\}) \cup N (\{T\}))$
Assertion	hdmapval2	$⊢ φ \to S (T) = I (⟨X, I (⟨E, J (E), X⟩), T⟩)$

Proof

Step	Hyp	Ref	Expression
1		hdmapval2.h	$⊢ H = LHyp (K)$
2		hdmapval2.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapval2.u	$⊢ U = DVecH (K) (W)$
4		hdmapval2.v	$⊢ V = {Base}_{U}$
5		hdmapval2.n	$⊢ N = LSpan (U)$
6		hdmapval2.c	$⊢ C = LCDual (K) (W)$
7		hdmapval2.d	$⊢ D = {Base}_{C}$
8		hdmapval2.j	$⊢ J = HVMap (K) (W)$
9		hdmapval2.i	$⊢ I = HDMap1 (K) (W)$
10		hdmapval2.s	$⊢ S = HDMap (K) (W)$
11		hdmapval2.k	$⊢ φ \to (K \in HL \land W \in H)$
12		hdmapval2.t	$⊢ φ \to T \in V$
13		hdmapval2.x	$⊢ φ \to X \in V$
14		hdmapval2.ne	$⊢ φ \to \neg X \in (N (\{E\}) \cup N (\{T\}))$
15		eqidd	$⊢ φ \to S (T) = S (T)$
16	1 3 4 6 7 10 11 12	hdmapcl	$⊢ φ \to S (T) \in D$
17	1 2 3 4 5 6 7 8 9 10 11 12 16	hdmapval2lem	$⊢ φ \to (S (T) = S (T) \leftrightarrow \forall z \in V (\neg z \in (N (\{E\}) \cup N (\{T\})) \to S (T) = I (⟨z, I (⟨E, J (E), z⟩), T⟩)))$
18	15 17	mpbid	$⊢ φ \to \forall z \in V (\neg z \in (N (\{E\}) \cup N (\{T\})) \to S (T) = I (⟨z, I (⟨E, J (E), z⟩), T⟩))$
19		eleq1	$⊢ z = X \to (z \in (N (\{E\}) \cup N (\{T\})) \leftrightarrow X \in (N (\{E\}) \cup N (\{T\})))$
20	19	notbid	$⊢ z = X \to (\neg z \in (N (\{E\}) \cup N (\{T\})) \leftrightarrow \neg X \in (N (\{E\}) \cup N (\{T\})))$
21		oteq1	$⊢ z = X \to ⟨z, I (⟨E, J (E), z⟩), T⟩ = ⟨X, I (⟨E, J (E), z⟩), T⟩$
22		oteq3	$⊢ z = X \to ⟨E, J (E), z⟩ = ⟨E, J (E), X⟩$
23	22	fveq2d	$⊢ z = X \to I (⟨E, J (E), z⟩) = I (⟨E, J (E), X⟩)$
24	23	oteq2d	$⊢ z = X \to ⟨X, I (⟨E, J (E), z⟩), T⟩ = ⟨X, I (⟨E, J (E), X⟩), T⟩$
25	21 24	eqtrd	$⊢ z = X \to ⟨z, I (⟨E, J (E), z⟩), T⟩ = ⟨X, I (⟨E, J (E), X⟩), T⟩$
26	25	fveq2d	$⊢ z = X \to I (⟨z, I (⟨E, J (E), z⟩), T⟩) = I (⟨X, I (⟨E, J (E), X⟩), T⟩)$
27	26	eqeq2d	$⊢ z = X \to (S (T) = I (⟨z, I (⟨E, J (E), z⟩), T⟩) \leftrightarrow S (T) = I (⟨X, I (⟨E, J (E), X⟩), T⟩))$
28	20 27	imbi12d	$⊢ z = X \to ((\neg z \in (N (\{E\}) \cup N (\{T\})) \to S (T) = I (⟨z, I (⟨E, J (E), z⟩), T⟩)) \leftrightarrow (\neg X \in (N (\{E\}) \cup N (\{T\})) \to S (T) = I (⟨X, I (⟨E, J (E), X⟩), T⟩)))$
29	28	rspccv	$⊢ \forall z \in V (\neg z \in (N (\{E\}) \cup N (\{T\})) \to S (T) = I (⟨z, I (⟨E, J (E), z⟩), T⟩)) \to (X \in V \to (\neg X \in (N (\{E\}) \cup N (\{T\})) \to S (T) = I (⟨X, I (⟨E, J (E), X⟩), T⟩)))$
30	18 13 14 29	syl3c	$⊢ φ \to S (T) = I (⟨X, I (⟨E, J (E), X⟩), T⟩)$

Metamath Proof Explorer

Theorem hdmapval2

Proof