Theorem mapdh75fN

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

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

Proof

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