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 )