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 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
Assertion axlowdimlem12 
|- ( ( K e. ( 1 ... N ) /\ K =/= ( I + 1 ) ) -> ( Q ` K ) = 0 )

Proof

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