Theorem axlowdimlem9

Description: Lemma for axlowdim . Calculate the value of P away from three. (Contributed by Scott Fenton, 21-Apr-2013)

	Ref	Expression
Hypothesis	axlowdimlem7.1	$$⊢P=\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)$$
Assertion	axlowdimlem9	$$⊢\left(K\in \left(1\dots N\right)\wedge K\ne 3\right)\to P\left(K\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem7.1	$$⊢P=\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)$$
2	1	fveq1i	$$⊢P\left(K\right)=\left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(K\right)$$
3		eldifsn	$$⊢K\in \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\leftrightarrow \left(K\in \left(1\dots N\right)\wedge K\ne 3\right)$$
4		disjdif	$$⊢\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing$$
5		3ex	$$⊢3\in \mathrm{V}$$
6		negex	$$⊢-1\in \mathrm{V}$$
7	5 6	fnsn	$$⊢\left\{⟨3,-1⟩\right\}Fn\left\{3\right\}$$
8		c0ex	$$⊢0\in \mathrm{V}$$
9	8	fconst	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶\left\{0\right\}$$
10		ffn	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶\left\{0\right\}\to \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)Fn\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)$$
11	9 10	ax-mp	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)Fn\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)$$
12		fvun2	$$⊢\left(\left\{⟨3,-1⟩\right\}Fn\left\{3\right\}\wedge \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)Fn\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\wedge \left(\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing \wedge K\in \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\right)\right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(K\right)=\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\left(K\right)$$
13	7 11 12	mp3an12	$$⊢\left(\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing \wedge K\in \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(K\right)=\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\left(K\right)$$
14	4 13	mpan	$$⊢K\in \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(K\right)=\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\left(K\right)$$
15	8	fvconst2	$$⊢K\in \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\to \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\left(K\right)=0$$
16	14 15	eqtrd	$$⊢K\in \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(K\right)=0$$
17	3 16	sylbir	$$⊢\left(K\in \left(1\dots N\right)\wedge K\ne 3\right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(K\right)=0$$
18	2 17	syl5eq	$$⊢\left(K\in \left(1\dots N\right)\wedge K\ne 3\right)\to P\left(K\right)=0$$