MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axlowdimlem12 Structured version   Unicode version

Theorem axlowdimlem12 23320
Description: Lemma for axlowdim 23328. Calculate the value of  Q away from its distinguished point. (Contributed by Scott Fenton, 21-Apr-2013.)
Hypothesis
Ref Expression
axlowdimlem10.1  |-  Q  =  ( { <. (
I  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( I  + 
1 ) } )  X.  { 0 } ) )
Assertion
Ref Expression
axlowdimlem12  |-  ( ( K  e.  ( 1 ... N )  /\  K  =/=  ( I  + 
1 ) )  -> 
( Q `  K
)  =  0 )

Proof of Theorem axlowdimlem12
StepHypRef Expression
1 axlowdimlem10.1 . . 3  |-  Q  =  ( { <. (
I  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( I  + 
1 ) } )  X.  { 0 } ) )
21fveq1i 5776 . 2  |-  ( Q `
 K )  =  ( ( { <. ( I  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( I  + 
1 ) } )  X.  { 0 } ) ) `  K
)
3 eldifsn 4084 . . 3  |-  ( K  e.  ( ( 1 ... N )  \  { ( I  + 
1 ) } )  <-> 
( K  e.  ( 1 ... N )  /\  K  =/=  (
I  +  1 ) ) )
4 disjdif 3835 . . . . 5  |-  ( { ( I  +  1 ) }  i^i  (
( 1 ... N
)  \  { (
I  +  1 ) } ) )  =  (/)
5 ovex 6201 . . . . . . 7  |-  ( I  +  1 )  e. 
_V
6 1ex 9468 . . . . . . 7  |-  1  e.  _V
75, 6fnsn 5555 . . . . . 6  |-  { <. ( I  +  1 ) ,  1 >. }  Fn  { ( I  +  1 ) }
8 c0ex 9467 . . . . . . . 8  |-  0  e.  _V
98fconst 5680 . . . . . . 7  |-  ( ( ( 1 ... N
)  \  { (
I  +  1 ) } )  X.  {
0 } ) : ( ( 1 ... N )  \  {
( I  +  1 ) } ) --> { 0 }
10 ffn 5643 . . . . . . 7  |-  ( ( ( ( 1 ... N )  \  {
( I  +  1 ) } )  X. 
{ 0 } ) : ( ( 1 ... N )  \  { ( I  + 
1 ) } ) --> { 0 }  ->  ( ( ( 1 ... N )  \  {
( I  +  1 ) } )  X. 
{ 0 } )  Fn  ( ( 1 ... N )  \  { ( I  + 
1 ) } ) )
119, 10ax-mp 5 . . . . . 6  |-  ( ( ( 1 ... N
)  \  { (
I  +  1 ) } )  X.  {
0 } )  Fn  ( ( 1 ... N )  \  {
( I  +  1 ) } )
12 fvun2 5848 . . . . . 6  |-  ( ( { <. ( 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 ) )
137, 11, 12mp3an12 1305 . . . . 5  |-  ( ( ( { ( 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
) )
144, 13mpan 670 . . . 4  |-  ( K  e.  ( ( 1 ... N )  \  { ( I  + 
1 ) } )  ->  ( ( {
<. ( I  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
I  +  1 ) } )  X.  {
0 } ) ) `
 K )  =  ( ( ( ( 1 ... N ) 
\  { ( I  +  1 ) } )  X.  { 0 } ) `  K
) )
158fvconst2 6018 . . . 4  |-  ( K  e.  ( ( 1 ... N )  \  { ( I  + 
1 ) } )  ->  ( ( ( ( 1 ... N
)  \  { (
I  +  1 ) } )  X.  {
0 } ) `  K )  =  0 )
1614, 15eqtrd 2490 . . 3  |-  ( K  e.  ( ( 1 ... N )  \  { ( I  + 
1 ) } )  ->  ( ( {
<. ( I  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
I  +  1 ) } )  X.  {
0 } ) ) `
 K )  =  0 )
173, 16sylbir 213 . 2  |-  ( ( K  e.  ( 1 ... N )  /\  K  =/=  ( I  + 
1 ) )  -> 
( ( { <. ( I  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( I  + 
1 ) } )  X.  { 0 } ) ) `  K
)  =  0 )
182, 17syl5eq 2502 1  |-  ( ( K  e.  ( 1 ... N )  /\  K  =/=  ( I  + 
1 ) )  -> 
( Q `  K
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1757    =/= wne 2641    \ cdif 3409    u. cun 3410    i^i cin 3411   (/)c0 3721   {csn 3961   <.cop 3967    X. cxp 4922    Fn wfn 5497   -->wf 5498   ` cfv 5502  (class class class)co 6176   0cc0 9369   1c1 9370    + caddc 9372   ...cfz 11524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615  ax-1cn 9427  ax-icn 9428  ax-addcl 9429  ax-mulcl 9431  ax-i2m1 9437
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-mpt 4436  df-id 4720  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-res 4936  df-ima 4937  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-fv 5510  df-ov 6179
This theorem is referenced by:  axlowdimlem14  23322  axlowdimlem16  23324  axlowdimlem17  23325
  Copyright terms: Public domain W3C validator