Metamath Proof Explorer

Theorem axlowdimlem12

Description: Lemma for axlowdim . Calculate the value of Q away from its distinguished point. (Contributed by Scott Fenton, 21-Apr-2013)

		Ref	Expression
	Hypothesis	axlowdimlem10.1	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
	Assertion	axlowdimlem12	$⊢ (K \in (1 \dots N) \land K \neq I + 1) \to Q (K) = 0$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem10.1	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
2	1	fveq1i	$⊢ Q (K) = (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) (K)$
3		eldifsn	$⊢ K \in ((1 \dots N) ∖ \{I + 1\}) \leftrightarrow (K \in (1 \dots N) \land K \neq I + 1)$
4		disjdif	$⊢ \{I + 1\} \cap ((1 \dots N) ∖ \{I + 1\}) = \emptyset$
5		ovex	$⊢ I + 1 \in V$
6		1ex	$⊢ 1 \in V$
7	5 6	fnsn	$⊢ \{⟨I + 1, 1⟩\} Fn \{I + 1\}$
8		c0ex	$⊢ 0 \in V$
9	8	fconst	$⊢ (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) : (1 \dots N) ∖ \{I + 1\} ⟶ \{0\}$
10		ffn	$⊢ (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) : (1 \dots N) ∖ \{I + 1\} ⟶ \{0\} \to (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) Fn ((1 \dots N) ∖ \{I + 1\})$
11	9 10	ax-mp	$⊢ (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) Fn ((1 \dots N) ∖ \{I + 1\})$
12		fvun2	$⊢ (\{⟨I + 1, 1⟩\} Fn \{I + 1\} \land (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) Fn ((1 \dots N) ∖ \{I + 1\}) \land (\{I + 1\} \cap ((1 \dots N) ∖ \{I + 1\}) = \emptyset \land K \in ((1 \dots N) ∖ \{I + 1\}))) \to (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) (K) = (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) (K)$
13	7 11 12	mp3an12	$⊢ (\{I + 1\} \cap ((1 \dots N) ∖ \{I + 1\}) = \emptyset \land K \in ((1 \dots N) ∖ \{I + 1\})) \to (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) (K) = (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) (K)$
14	4 13	mpan	$⊢ K \in ((1 \dots N) ∖ \{I + 1\}) \to (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) (K) = (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) (K)$
15	8	fvconst2	$⊢ K \in ((1 \dots N) ∖ \{I + 1\}) \to (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) (K) = 0$
16	14 15	eqtrd	$⊢ K \in ((1 \dots N) ∖ \{I + 1\}) \to (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) (K) = 0$
17	3 16	sylbir	$⊢ (K \in (1 \dots N) \land K \neq I + 1) \to (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) (K) = 0$
18	2 17	syl5eq	$⊢ (K \in (1 \dots N) \land K \neq I + 1) \to Q (K) = 0$