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

Proof

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