Theorem mapdh7dN

Description: Part (7) of Baer p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdh7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdh7.v	$$⊢V={\mathrm{Base}}_U$$
	mapdh7.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdh7.o	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdh7.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdh7.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdh7.d	$$⊢D={\mathrm{Base}}_C$$
	mapdh7.r	$$⊢R={-}_C$$
	mapdh7.q	$$⊢Q=0_C$$
	mapdh7.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdh7.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdh7.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)$$
	mapdh7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdh7.f	$$⊢\phi \to F\in D$$
	mapdh7.mn	$$⊢\phi \to M\left(N\left(\left\{u\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
	mapdh7.x	$$⊢\phi \to u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh7.y	$$⊢\phi \to v\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh7.z	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh7.ne	$$⊢\phi \to N\left(\left\{u\right\}\right)\ne N\left(\left\{v\right\}\right)$$
	mapdh7.wn	$$⊢\phi \to \neg w\in N\left(\left\{u,v\right\}\right)$$
	mapdh7a	$$⊢\phi \to I\left(⟨u,F,v⟩\right)=G$$
	mapdh7.b	$$⊢\phi \to I\left(⟨u,F,w⟩\right)=E$$
Assertion	mapdh7dN	$$⊢\phi \to I\left(⟨v,G,w⟩\right)=E$$

Proof

Step	Hyp	Ref	Expression
1		mapdh7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdh7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapdh7.v	$$⊢V={\mathrm{Base}}_U$$
4		mapdh7.s	$$⊢\underset{\dot{}}{-}={-}_U$$
5		mapdh7.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		mapdh7.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		mapdh7.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		mapdh7.d	$$⊢D={\mathrm{Base}}_C$$
9		mapdh7.r	$$⊢R={-}_C$$
10		mapdh7.q	$$⊢Q=0_C$$
11		mapdh7.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
12		mapdh7.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
13		mapdh7.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		mapdh7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15		mapdh7.f	$$⊢\phi \to F\in D$$
16		mapdh7.mn	$$⊢\phi \to M\left(N\left(\left\{u\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
17		mapdh7.x	$$⊢\phi \to u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		mapdh7.y	$$⊢\phi \to v\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		mapdh7.z	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
20		mapdh7.ne	$$⊢\phi \to N\left(\left\{u\right\}\right)\ne N\left(\left\{v\right\}\right)$$
21		mapdh7.wn	$$⊢\phi \to \neg w\in N\left(\left\{u,v\right\}\right)$$
22		mapdh7a	$$⊢\phi \to I\left(⟨u,F,v⟩\right)=G$$
23		mapdh7.b	$$⊢\phi \to I\left(⟨u,F,w⟩\right)=E$$
24	1 2 14	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
25	18	eldifad	$$⊢\phi \to v\in V$$
26	19	eldifad	$$⊢\phi \to w\in V$$
27	3 5 6 24 17 25 26 20 21	lspindp1	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{v\right\}\right)\wedge \neg u\in N\left(\left\{w,v\right\}\right)\right)$$
28	27	simprd	$$⊢\phi \to \neg u\in N\left(\left\{w,v\right\}\right)$$
29		prcom	$$⊢\left\{v,w\right\}=\left\{w,v\right\}$$
30	29	fveq2i	$$⊢N\left(\left\{v,w\right\}\right)=N\left(\left\{w,v\right\}\right)$$
31	30	eleq2i	$$⊢u\in N\left(\left\{v,w\right\}\right)\leftrightarrow u\in N\left(\left\{w,v\right\}\right)$$
32	28 31	sylnibr	$$⊢\phi \to \neg u\in N\left(\left\{v,w\right\}\right)$$
33	17	eldifad	$$⊢\phi \to u\in V$$
34	3 6 24 26 33 25 21	lspindpi	$$⊢\phi \to \left(N\left(\left\{w\right\}\right)\ne N\left(\left\{u\right\}\right)\wedge N\left(\left\{w\right\}\right)\ne N\left(\left\{v\right\}\right)\right)$$
35	34	simprd	$$⊢\phi \to N\left(\left\{w\right\}\right)\ne N\left(\left\{v\right\}\right)$$
36	35	necomd	$$⊢\phi \to N\left(\left\{v\right\}\right)\ne N\left(\left\{w\right\}\right)$$
37	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 17 18 19 32 36 22 23	mapdheq4	$$⊢\phi \to I\left(⟨v,G,w⟩\right)=E$$