Theorem axlowdimlem12 27016

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

Hypothesis

Ref	Expression
axlowdimlem10.1	⊢ 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))

Assertion

Ref	Expression
axlowdimlem12	⊢ ((𝐾 ∈ (1...𝑁) ∧ 𝐾 ≠ (𝐼 + 1)) → (𝑄‘𝐾) = 0)

Proof of Theorem axlowdimlem12

Step	Hyp	Ref	Expression
1		axlowdimlem10.1	. . 3 ⊢ 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))
2	1	fveq1i 6707	. 2 ⊢ (𝑄‘𝐾) = (({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))‘𝐾)
3		eldifsn 4690	. . 3 ⊢ (𝐾 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}) ↔ (𝐾 ∈ (1...𝑁) ∧ 𝐾 ≠ (𝐼 + 1)))
4		disjdif 4376	. . . . 5 ⊢ ({(𝐼 + 1)} ∩ ((1...𝑁) ∖ {(𝐼 + 1)})) = ∅
5		ovex 7235	. . . . . . 7 ⊢ (𝐼 + 1) ∈ V
6		1ex 10812	. . . . . . 7 ⊢ 1 ∈ V
7	5, 6	fnsn 6427	. . . . . 6 ⊢ {⟨(𝐼 + 1), 1⟩} Fn {(𝐼 + 1)}
8		c0ex 10810	. . . . . . . 8 ⊢ 0 ∈ V
9	8	fconst 6594	. . . . . . 7 ⊢ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}):((1...𝑁) ∖ {(𝐼 + 1)})⟶{0}
10		ffn 6534	. . . . . . 7 ⊢ ((((1...𝑁) ∖ {(𝐼 + 1)}) × {0}):((1...𝑁) ∖ {(𝐼 + 1)})⟶{0} → (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}) Fn ((1...𝑁) ∖ {(𝐼 + 1)}))
11	9, 10	ax-mp 5	. . . . . 6 ⊢ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}) Fn ((1...𝑁) ∖ {(𝐼 + 1)})
12		fvun2 6792	. . . . . 6 ⊢ (({⟨(𝐼 + 1), 1⟩} Fn {(𝐼 + 1)} ∧ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}) Fn ((1...𝑁) ∖ {(𝐼 + 1)}) ∧ (({(𝐼 + 1)} ∩ ((1...𝑁) ∖ {(𝐼 + 1)})) = ∅ ∧ 𝐾 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}))) → (({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))‘𝐾) = ((((1...𝑁) ∖ {(𝐼 + 1)}) × {0})‘𝐾))
13	7, 11, 12	mp3an12 1453	. . . . 5 ⊢ ((({(𝐼 + 1)} ∩ ((1...𝑁) ∖ {(𝐼 + 1)})) = ∅ ∧ 𝐾 ∈ ((1...𝑁) ∖ {(𝐼 + 1)})) → (({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))‘𝐾) = ((((1...𝑁) ∖ {(𝐼 + 1)}) × {0})‘𝐾))
14	4, 13	mpan 690	. . . 4 ⊢ (𝐾 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}) → (({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))‘𝐾) = ((((1...𝑁) ∖ {(𝐼 + 1)}) × {0})‘𝐾))
15	8	fvconst2 7008	. . . 4 ⊢ (𝐾 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}) → ((((1...𝑁) ∖ {(𝐼 + 1)}) × {0})‘𝐾) = 0)
16	14, 15	eqtrd 2774	. . 3 ⊢ (𝐾 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}) → (({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))‘𝐾) = 0)
17	3, 16	sylbir 238	. 2 ⊢ ((𝐾 ∈ (1...𝑁) ∧ 𝐾 ≠ (𝐼 + 1)) → (({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))‘𝐾) = 0)
18	2, 17	syl5eq 2786	1 ⊢ ((𝐾 ∈ (1...𝑁) ∧ 𝐾 ≠ (𝐼 + 1)) → (𝑄‘𝐾) = 0)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   ≠ wne 2935   ∖ cdif 3854   ∪ cun 3855   ∩ cin 3856  ∅c0 4227  {csn 4531  ⟨cop 4537   × cxp 5538   Fn wfn 6364  ⟶wf 6365  ‘cfv 6369  (class class class)co 7202  0cc0 10712  1c1 10713   + caddc 10715  ...cfz 13078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pr 5311  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-mulcl 10774  ax-i2m1 10780

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3403  df-sbc 3688  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-fv 6377  df-ov 7205

This theorem is referenced by:  axlowdimlem14  27018  axlowdimlem16  27020  axlowdimlem17  27021