Theorem 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=\mathrm{LHyp}\left(K\right)$$
	mapdh8a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdh8a.v	$$⊢V={\mathrm{Base}}_U$$
	mapdh8a.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdh8a.o	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdh8a.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdh8a.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdh8a.d	$$⊢D={\mathrm{Base}}_C$$
	mapdh8a.r	$$⊢R={-}_C$$
	mapdh8a.q	$$⊢Q=0_C$$
	mapdh8a.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdh8a.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdh8a.i	$$⊢I=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
	mapdh8a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdh8h.f	$$⊢\phi \to F\in D$$
	mapdh8h.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
	mapdh8i.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh8i.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh8i.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh8i.xy	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	mapdh8i.xz	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
	mapdh8i.yt	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{T\right\}\right)$$
	mapdh8i.zt	$$⊢\phi \to N\left(\left\{Z\right\}\right)\ne N\left(\left\{T\right\}\right)$$
	mapdh8.t	$$⊢\phi \to T\in V$$
Assertion	mapdh8	$$⊢\phi \to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),T⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),T⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdh8a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdh8a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapdh8a.v	$$⊢V={\mathrm{Base}}_U$$
4		mapdh8a.s	$$⊢\underset{\dot{}}{-}={-}_U$$
5		mapdh8a.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		mapdh8a.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		mapdh8a.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		mapdh8a.d	$$⊢D={\mathrm{Base}}_C$$
9		mapdh8a.r	$$⊢R={-}_C$$
10		mapdh8a.q	$$⊢Q=0_C$$
11		mapdh8a.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
12		mapdh8a.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
13		mapdh8a.i	$$⊢I=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
14		mapdh8a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15		mapdh8h.f	$$⊢\phi \to F\in D$$
16		mapdh8h.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
17		mapdh8i.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		mapdh8i.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		mapdh8i.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
20		mapdh8i.xy	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
21		mapdh8i.xz	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
22		mapdh8i.yt	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{T\right\}\right)$$
23		mapdh8i.zt	$$⊢\phi \to N\left(\left\{Z\right\}\right)\ne N\left(\left\{T\right\}\right)$$
24		mapdh8.t	$$⊢\phi \to T\in V$$
25		fvexd	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in \mathrm{V}$$
26	10 13 5 18 25	mapdhval0	$$⊢\phi \to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),\underset{\dot{}}{0}⟩\right)=Q$$
27		fvexd	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)\in \mathrm{V}$$
28	10 13 5 19 27	mapdhval0	$$⊢\phi \to I\left(⟨Z,I\left(⟨X,F,Z⟩\right),\underset{\dot{}}{0}⟩\right)=Q$$
29	26 28	eqtr4d	$$⊢\phi \to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),\underset{\dot{}}{0}⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),\underset{\dot{}}{0}⟩\right)$$
30	29	adantr	$$⊢\left(\phi \wedge T=\underset{\dot{}}{0}\right)\to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),\underset{\dot{}}{0}⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),\underset{\dot{}}{0}⟩\right)$$
31		oteq3	$$⊢T=\underset{\dot{}}{0}\to ⟨Y,I\left(⟨X,F,Y⟩\right),T⟩=⟨Y,I\left(⟨X,F,Y⟩\right),\underset{\dot{}}{0}⟩$$
32	31	fveq2d	$$⊢T=\underset{\dot{}}{0}\to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),T⟩\right)=I\left(⟨Y,I\left(⟨X,F,Y⟩\right),\underset{\dot{}}{0}⟩\right)$$
33	32	adantl	$$⊢\left(\phi \wedge T=\underset{\dot{}}{0}\right)\to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),T⟩\right)=I\left(⟨Y,I\left(⟨X,F,Y⟩\right),\underset{\dot{}}{0}⟩\right)$$
34		oteq3	$$⊢T=\underset{\dot{}}{0}\to ⟨Z,I\left(⟨X,F,Z⟩\right),T⟩=⟨Z,I\left(⟨X,F,Z⟩\right),\underset{\dot{}}{0}⟩$$
35	34	fveq2d	$$⊢T=\underset{\dot{}}{0}\to I\left(⟨Z,I\left(⟨X,F,Z⟩\right),T⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),\underset{\dot{}}{0}⟩\right)$$
36	35	adantl	$$⊢\left(\phi \wedge T=\underset{\dot{}}{0}\right)\to I\left(⟨Z,I\left(⟨X,F,Z⟩\right),T⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),\underset{\dot{}}{0}⟩\right)$$
37	30 33 36	3eqtr4d	$$⊢\left(\phi \wedge T=\underset{\dot{}}{0}\right)\to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),T⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),T⟩\right)$$
38	14	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
39	15	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to F\in D$$
40	16	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
41	17	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
42	18	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
43	19	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
44	20	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
45	21	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
46	22	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to N\left(\left\{Y\right\}\right)\ne N\left(\left\{T\right\}\right)$$
47	23	adantr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to N\left(\left\{Z\right\}\right)\ne N\left(\left\{T\right\}\right)$$
48	24	anim1i	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to \left(T\in V\wedge T\ne \underset{\dot{}}{0}\right)$$
49		eldifsn	$$⊢T\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(T\in V\wedge T\ne \underset{\dot{}}{0}\right)$$
50	48 49	sylibr	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to T\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
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	$$⊢\left(\phi \wedge T\ne \underset{\dot{}}{0}\right)\to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),T⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),T⟩\right)$$
52	37 51	pm2.61dane	$$⊢\phi \to I\left(⟨Y,I\left(⟨X,F,Y⟩\right),T⟩\right)=I\left(⟨Z,I\left(⟨X,F,Z⟩\right),T⟩\right)$$