Metamath Proof Explorer

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 = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
Assertion axlowdimlem9 
|- ( ( K e. ( 1 ... N ) /\ K =/= 3 ) -> ( P ` K ) = 0 )

Proof

Step Hyp Ref Expression
1 axlowdimlem7.1 
 |-  P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
2 1 fveq1i 
 |-  ( P ` K ) = ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` K )
3 eldifsn 
 |-  ( K e. ( ( 1 ... N ) \ { 3 } ) <-> ( K e. ( 1 ... N ) /\ K =/= 3 ) )
4 disjdif 
 |-  ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/)
5 3ex 
 |-  3 e. _V
6 negex 
 |-  -u 1 e. _V
7 5 6 fnsn 
 |-  { <. 3 , -u 1 >. } Fn { 3 }
8 c0ex 
 |-  0 e. _V
9 8 fconst 
 |-  ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> { 0 }
10 ffn 
 |-  ( ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> { 0 } -> ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { 3 } ) )
11 9 10 ax-mp 
 |-  ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { 3 } )
12 fvun2 
 |-  ( ( { <. 3 , -u 1 >. } Fn { 3 } /\ ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { 3 } ) /\ ( ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/) /\ K e. ( ( 1 ... N ) \ { 3 } ) ) ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` K ) = ( ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ` K ) )
13 7 11 12 mp3an12 
 |-  ( ( ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/) /\ K e. ( ( 1 ... N ) \ { 3 } ) ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` K ) = ( ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ` K ) )
14 4 13 mpan 
 |-  ( K e. ( ( 1 ... N ) \ { 3 } ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` K ) = ( ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ` K ) )
15 8 fvconst2 
 |-  ( K e. ( ( 1 ... N ) \ { 3 } ) -> ( ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ` K ) = 0 )
16 14 15 eqtrd 
 |-  ( K e. ( ( 1 ... N ) \ { 3 } ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` K ) = 0 )
17 3 16 sylbir 
 |-  ( ( K e. ( 1 ... N ) /\ K =/= 3 ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` K ) = 0 )
18 2 17 syl5eq 
 |-  ( ( K e. ( 1 ... N ) /\ K =/= 3 ) -> ( P ` K ) = 0 )