Metamath Proof Explorer

Theorem axlowdimlem13

Description: Lemma for axlowdim . Establish that P and Q are different points. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypotheses axlowdimlem13.1 
|- P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
axlowdimlem13.2 
|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
Assertion axlowdimlem13 
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> P =/= Q )

Proof

Step Hyp Ref Expression
1 axlowdimlem13.1 
 |-  P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
2 axlowdimlem13.2 
 |-  Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
3 2ne0 
 |-  2 =/= 0
4 3 neii 
 |-  -. 2 = 0
5 eqcom 
 |-  ( 2 = 0 <-> 0 = 2 )
6 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
7 6 eqcomi 
 |-  0 = ( 1 + -u 1 )
8 df-2 
 |-  2 = ( 1 + 1 )
9 7 8 eqeq12i 
 |-  ( 0 = 2 <-> ( 1 + -u 1 ) = ( 1 + 1 ) )
10 ax-1cn 
 |-  1 e. CC
11 neg1cn 
 |-  -u 1 e. CC
12 10 11 10 addcani 
 |-  ( ( 1 + -u 1 ) = ( 1 + 1 ) <-> -u 1 = 1 )
13 5 9 12 3bitri 
 |-  ( 2 = 0 <-> -u 1 = 1 )
14 4 13 mtbi 
 |-  -. -u 1 = 1
15 14 intnanr 
 |-  -. ( -u 1 = 1 /\ 0 = 0 )
16 ax-1ne0 
 |-  1 =/= 0
17 16 neii 
 |-  -. 1 = 0
18 negeq0 
 |-  ( 1 e. CC -> ( 1 = 0 <-> -u 1 = 0 ) )
19 10 18 ax-mp 
 |-  ( 1 = 0 <-> -u 1 = 0 )
20 17 19 mtbi 
 |-  -. -u 1 = 0
21 20 intnanr 
 |-  -. ( -u 1 = 0 /\ 0 = 1 )
22 15 21 pm3.2ni 
 |-  -. ( ( -u 1 = 1 /\ 0 = 0 ) \/ ( -u 1 = 0 /\ 0 = 1 ) )
23 negex 
 |-  -u 1 e. _V
24 c0ex 
 |-  0 e. _V
25 1ex 
 |-  1 e. _V
26 23 24 25 24 preq12b 
 |-  ( { -u 1 , 0 } = { 1 , 0 } <-> ( ( -u 1 = 1 /\ 0 = 0 ) \/ ( -u 1 = 0 /\ 0 = 1 ) ) )
27 22 26 mtbir 
 |-  -. { -u 1 , 0 } = { 1 , 0 }
28 3ex 
 |-  3 e. _V
29 28 rnsnop 
 |-  ran { <. 3 , -u 1 >. } = { -u 1 }
30 29 a1i 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran { <. 3 , -u 1 >. } = { -u 1 } )
31 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
32 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
33 31 32 sylbi 
 |-  ( N e. NN -> 1 e. ( 1 ... N ) )
34 df-3 
 |-  3 = ( 2 + 1 )
35 1e0p1 
 |-  1 = ( 0 + 1 )
36 34 35 eqeq12i 
 |-  ( 3 = 1 <-> ( 2 + 1 ) = ( 0 + 1 ) )
37 2cn 
 |-  2 e. CC
38 0cn 
 |-  0 e. CC
39 37 38 10 addcan2i 
 |-  ( ( 2 + 1 ) = ( 0 + 1 ) <-> 2 = 0 )
40 36 39 bitri 
 |-  ( 3 = 1 <-> 2 = 0 )
41 40 necon3bii 
 |-  ( 3 =/= 1 <-> 2 =/= 0 )
42 3 41 mpbir 
 |-  3 =/= 1
43 42 necomi 
 |-  1 =/= 3
44 eldifsn 
 |-  ( 1 e. ( ( 1 ... N ) \ { 3 } ) <-> ( 1 e. ( 1 ... N ) /\ 1 =/= 3 ) )
45 33 43 44 sylanblrc 
 |-  ( N e. NN -> 1 e. ( ( 1 ... N ) \ { 3 } ) )
46 45 adantr 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 e. ( ( 1 ... N ) \ { 3 } ) )
47 ne0i 
 |-  ( 1 e. ( ( 1 ... N ) \ { 3 } ) -> ( ( 1 ... N ) \ { 3 } ) =/= (/) )
48 rnxp 
 |-  ( ( ( 1 ... N ) \ { 3 } ) =/= (/) -> ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) = { 0 } )
49 46 47 48 3syl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) = { 0 } )
50 30 49 uneq12d 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ran { <. 3 , -u 1 >. } u. ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { -u 1 } u. { 0 } ) )
51 rnun 
 |-  ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( ran { <. 3 , -u 1 >. } u. ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
52 df-pr 
 |-  { -u 1 , 0 } = ( { -u 1 } u. { 0 } )
53 50 51 52 3eqtr4g 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = { -u 1 , 0 } )
54 ovex 
 |-  ( I + 1 ) e. _V
55 54 rnsnop 
 |-  ran { <. ( I + 1 ) , 1 >. } = { 1 }
56 55 a1i 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran { <. ( I + 1 ) , 1 >. } = { 1 } )
57 nnz 
 |-  ( N e. NN -> N e. ZZ )
58 fzssp1 
 |-  ( 1 ... ( N - 1 ) ) C_ ( 1 ... ( ( N - 1 ) + 1 ) )
59 zcn 
 |-  ( N e. ZZ -> N e. CC )
60 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
61 60 oveq2d 
 |-  ( N e. CC -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
62 59 61 syl 
 |-  ( N e. ZZ -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
63 58 62 sseqtrid 
 |-  ( N e. ZZ -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
64 57 63 syl 
 |-  ( N e. NN -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
65 64 sselda 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I e. ( 1 ... N ) )
66 elfzelz 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I e. ZZ )
67 66 zred 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I e. RR )
68 id 
 |-  ( I e. RR -> I e. RR )
69 ltp1 
 |-  ( I e. RR -> I < ( I + 1 ) )
70 68 69 ltned 
 |-  ( I e. RR -> I =/= ( I + 1 ) )
71 67 70 syl 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I =/= ( I + 1 ) )
72 71 adantl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I =/= ( I + 1 ) )
73 eldifsn 
 |-  ( I e. ( ( 1 ... N ) \ { ( I + 1 ) } ) <-> ( I e. ( 1 ... N ) /\ I =/= ( I + 1 ) ) )
74 65 72 73 sylanbrc 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I e. ( ( 1 ... N ) \ { ( I + 1 ) } ) )
75 ne0i 
 |-  ( I e. ( ( 1 ... N ) \ { ( I + 1 ) } ) -> ( ( 1 ... N ) \ { ( I + 1 ) } ) =/= (/) )
76 rnxp 
 |-  ( ( ( 1 ... N ) \ { ( I + 1 ) } ) =/= (/) -> ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) = { 0 } )
77 74 75 76 3syl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) = { 0 } )
78 56 77 uneq12d 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ran { <. ( I + 1 ) , 1 >. } u. ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) = ( { 1 } u. { 0 } ) )
79 rnun 
 |-  ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) = ( ran { <. ( I + 1 ) , 1 >. } u. ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
80 df-pr 
 |-  { 1 , 0 } = ( { 1 } u. { 0 } )
81 78 79 80 3eqtr4g 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) = { 1 , 0 } )
82 53 81 eqeq12d 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) <-> { -u 1 , 0 } = { 1 , 0 } ) )
83 27 82 mtbiri 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> -. ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) )
84 rneq 
 |-  ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) -> ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) )
85 83 84 nsyl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> -. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) )
86 1 2 eqeq12i 
 |-  ( P = Q <-> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) )
87 86 necon3abii 
 |-  ( P =/= Q <-> -. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) )
88 85 87 sylibr 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> P =/= Q )