mapdh8

Description: Part (8) in Baer p. 48. Given a reference vector X , the value of function I at a vector T is independent of the choice of auxiliary vectors Y and Z . Unlike Baer's, our version does not require X , Y , and Z to be independent, and also is defined for all Y and Z that are not colinear with X or T . We do this to make the definition of Baer's sigma function more straightforward. (This part eliminates T =/= .0. .) (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)$
	mapdh8h.f	$⊢ φ \to F \in D$
	mapdh8h.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh8i.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8i.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8i.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdh8i.xy	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdh8i.xz	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
	mapdh8i.yt	$⊢ φ \to N (\{Y\}) \neq N (\{T\})$
	mapdh8i.zt	$⊢ φ \to N (\{Z\}) \neq N (\{T\})$
	mapdh8.t	$⊢ φ \to T \in V$
Assertion	mapdh8	$⊢ φ \to I (⟨Y, I (⟨X, F, Y⟩), T⟩) = I (⟨Z, I (⟨X, F, Z⟩), 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		mapdh8h.f	$⊢ φ \to F \in D$
16		mapdh8h.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh8i.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		mapdh8i.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
19		mapdh8i.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
20		mapdh8i.xy	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
21		mapdh8i.xz	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
22		mapdh8i.yt	$⊢ φ \to N (\{Y\}) \neq N (\{T\})$
23		mapdh8i.zt	$⊢ φ \to N (\{Z\}) \neq N (\{T\})$
24		mapdh8.t	$⊢ φ \to T \in V$
25		fvexd	$⊢ φ \to I (⟨X, F, Y⟩) \in V$
26	10 13 5 18 25	mapdhval0	$⊢ φ \to I (⟨Y, I (⟨X, F, Y⟩), \underset{˙}{0}⟩) = Q$
27		fvexd	$⊢ φ \to I (⟨X, F, Z⟩) \in V$
28	10 13 5 19 27	mapdhval0	$⊢ φ \to I (⟨Z, I (⟨X, F, Z⟩), \underset{˙}{0}⟩) = Q$
29	26 28	eqtr4d	$⊢ φ \to I (⟨Y, I (⟨X, F, Y⟩), \underset{˙}{0}⟩) = I (⟨Z, I (⟨X, F, Z⟩), \underset{˙}{0}⟩)$
30	29	adantr	$⊢ (φ \land T = \underset{˙}{0}) \to I (⟨Y, I (⟨X, F, Y⟩), \underset{˙}{0}⟩) = I (⟨Z, I (⟨X, F, Z⟩), \underset{˙}{0}⟩)$
31		oteq3	$⊢ T = \underset{˙}{0} \to ⟨Y, I (⟨X, F, Y⟩), T⟩ = ⟨Y, I (⟨X, F, Y⟩), \underset{˙}{0}⟩$
32	31	fveq2d	$⊢ T = \underset{˙}{0} \to I (⟨Y, I (⟨X, F, Y⟩), T⟩) = I (⟨Y, I (⟨X, F, Y⟩), \underset{˙}{0}⟩)$
33	32	adantl	$⊢ (φ \land T = \underset{˙}{0}) \to I (⟨Y, I (⟨X, F, Y⟩), T⟩) = I (⟨Y, I (⟨X, F, Y⟩), \underset{˙}{0}⟩)$
34		oteq3	$⊢ T = \underset{˙}{0} \to ⟨Z, I (⟨X, F, Z⟩), T⟩ = ⟨Z, I (⟨X, F, Z⟩), \underset{˙}{0}⟩$
35	34	fveq2d	$⊢ T = \underset{˙}{0} \to I (⟨Z, I (⟨X, F, Z⟩), T⟩) = I (⟨Z, I (⟨X, F, Z⟩), \underset{˙}{0}⟩)$
36	35	adantl	$⊢ (φ \land T = \underset{˙}{0}) \to I (⟨Z, I (⟨X, F, Z⟩), T⟩) = I (⟨Z, I (⟨X, F, Z⟩), \underset{˙}{0}⟩)$
37	30 33 36	3eqtr4d	$⊢ (φ \land T = \underset{˙}{0}) \to I (⟨Y, I (⟨X, F, Y⟩), T⟩) = I (⟨Z, I (⟨X, F, Z⟩), T⟩)$
38	14	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to (K \in HL \land W \in H)$
39	15	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to F \in D$
40	16	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to M (N (\{X\})) = J (\{F\})$
41	17	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
42	18	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to Y \in (V ∖ \{\underset{˙}{0}\})$
43	19	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to Z \in (V ∖ \{\underset{˙}{0}\})$
44	20	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y\})$
45	21	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Z\})$
46	22	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to N (\{Y\}) \neq N (\{T\})$
47	23	adantr	$⊢ (φ \land T \neq \underset{˙}{0}) \to N (\{Z\}) \neq N (\{T\})$
48	24	anim1i	$⊢ (φ \land T \neq \underset{˙}{0}) \to (T \in V \land T \neq \underset{˙}{0})$
49		eldifsn	$⊢ T \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (T \in V \land T \neq \underset{˙}{0})$
50	48 49	sylibr	$⊢ (φ \land T \neq \underset{˙}{0}) \to T \in (V ∖ \{\underset{˙}{0}\})$
51	1 2 3 4 5 6 7 8 9 10 11 12 13 38 39 40 41 42 43 44 45 46 47 50	mapdh8j	$⊢ (φ \land T \neq \underset{˙}{0}) \to I (⟨Y, I (⟨X, F, Y⟩), T⟩) = I (⟨Z, I (⟨X, F, Z⟩), T⟩)$
52	37 51	pm2.61dane	$⊢ φ \to I (⟨Y, I (⟨X, F, Y⟩), T⟩) = I (⟨Z, I (⟨X, F, Z⟩), T⟩)$

Metamath Proof Explorer

Theorem mapdh8

Proof