Theorem mapdhval2

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Hypotheses	mapdh.q	$$⊢Q=0_C$$
	mapdh.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)$$
	mapdh2.x	$$⊢\phi \to X\in A$$
	mapdh2.f	$$⊢\phi \to F\in B$$
	mapdh2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	mapdhval2	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$$⊢Q=0_C$$
2		mapdh.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)$$
3		mapdh2.x	$$⊢\phi \to X\in A$$
4		mapdh2.f	$$⊢\phi \to F\in B$$
5		mapdh2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
6	1 2 3 4 5	mapdhval	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=if\left(Y=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)\right)$$
7		eldifsni	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to Y\ne \underset{\dot{}}{0}$$
8	7	neneqd	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \neg Y=\underset{\dot{}}{0}$$
9		iffalse	$$⊢\neg Y=\underset{\dot{}}{0}\to if\left(Y=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)$$
10	5 8 9	3syl	$$⊢\phi \to if\left(Y=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)$$
11	6 10	eqtrd	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)$$