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	⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
Assertion	axlowdimlem12	⊢ ( ( 𝐾 ∈ ( 1 ... 𝑁 ) ∧ 𝐾 ≠ ( 𝐼 + 1 ) ) → ( 𝑄 ‘ 𝐾 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem10.1	⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
2	1	fveq1i	⊢ ( 𝑄 ‘ 𝐾 ) = ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ 𝐾 )
3		eldifsn	⊢ ( 𝐾 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ↔ ( 𝐾 ∈ ( 1 ... 𝑁 ) ∧ 𝐾 ≠ ( 𝐼 + 1 ) ) )
4		disjdif	⊢ ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅
5		ovex	⊢ ( 𝐼 + 1 ) ∈ V
6		1ex	⊢ 1 ∈ V
7	5 6	fnsn	⊢ { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } Fn { ( 𝐼 + 1 ) }
8		c0ex	⊢ 0 ∈ V
9	8	fconst	⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 }
10		ffn	⊢ ( ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 } → ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) )
11	9 10	ax-mp	⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } )
12		fvun2	⊢ ( ( { ⟨ ( 𝐼 + 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	⊢ ( ( ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅ ∧ 𝐾 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) → ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ 𝐾 ) = ( ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ‘ 𝐾 ) )
14	4 13	mpan	⊢ ( 𝐾 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) → ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ 𝐾 ) = ( ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ‘ 𝐾 ) )
15	8	fvconst2	⊢ ( 𝐾 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) → ( ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ‘ 𝐾 ) = 0 )
16	14 15	eqtrd	⊢ ( 𝐾 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) → ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ 𝐾 ) = 0 )
17	3 16	sylbir	⊢ ( ( 𝐾 ∈ ( 1 ... 𝑁 ) ∧ 𝐾 ≠ ( 𝐼 + 1 ) ) → ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ 𝐾 ) = 0 )
18	2 17	syl5eq	⊢ ( ( 𝐾 ∈ ( 1 ... 𝑁 ) ∧ 𝐾 ≠ ( 𝐼 + 1 ) ) → ( 𝑄 ‘ 𝐾 ) = 0 )