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 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
axlowdimlem13.2 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
Assertion axlowdimlem13 ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑃 ≠ 𝑄 )

Proof

Step Hyp Ref Expression
1 axlowdimlem13.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
2 axlowdimlem13.2 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
3 2ne0 ⊢ 2 ≠ 0
4 3 neii ⊢ ¬ 2 = 0
5 eqcom ⊢ ( 2 = 0 ↔ 0 = 2 )
6 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
7 6 eqcomi ⊢ 0 = ( 1 + - 1 )
8 df-2 ⊢ 2 = ( 1 + 1 )
9 7 8 eqeq12i ⊢ ( 0 = 2 ↔ ( 1 + - 1 ) = ( 1 + 1 ) )
10 ax-1cn ⊢ 1 ∈ ℂ
11 neg1cn ⊢ - 1 ∈ ℂ
12 10 11 10 addcani ⊢ ( ( 1 + - 1 ) = ( 1 + 1 ) ↔ - 1 = 1 )
13 5 9 12 3bitri ⊢ ( 2 = 0 ↔ - 1 = 1 )
14 4 13 mtbi ⊢ ¬ - 1 = 1
15 14 intnanr ⊢ ¬ ( - 1 = 1 ∧ 0 = 0 )
16 ax-1ne0 ⊢ 1 ≠ 0
17 16 neii ⊢ ¬ 1 = 0
18 negeq0 ⊢ ( 1 ∈ ℂ → ( 1 = 0 ↔ - 1 = 0 ) )
19 10 18 ax-mp ⊢ ( 1 = 0 ↔ - 1 = 0 )
20 17 19 mtbi ⊢ ¬ - 1 = 0
21 20 intnanr ⊢ ¬ ( - 1 = 0 ∧ 0 = 1 )
22 15 21 pm3.2ni ⊢ ¬ ( ( - 1 = 1 ∧ 0 = 0 ) ∨ ( - 1 = 0 ∧ 0 = 1 ) )
23 negex ⊢ - 1 ∈ V
24 c0ex ⊢ 0 ∈ V
25 1ex ⊢ 1 ∈ V
26 23 24 25 24 preq12b ⊢ ( { - 1 , 0 } = { 1 , 0 } ↔ ( ( - 1 = 1 ∧ 0 = 0 ) ∨ ( - 1 = 0 ∧ 0 = 1 ) ) )
27 22 26 mtbir ⊢ ¬ { - 1 , 0 } = { 1 , 0 }
28 3ex ⊢ 3 ∈ V
29 28 rnsnop ⊢ ran { ⟨ 3 , - 1 ⟩ } = { - 1 }
30 29 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ran { ⟨ 3 , - 1 ⟩ } = { - 1 } )
31 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
32 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
33 31 32 sylbi ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ( 1 ... 𝑁 ) )
34 df-3 ⊢ 3 = ( 2 + 1 )
35 1e0p1 ⊢ 1 = ( 0 + 1 )
36 34 35 eqeq12i ⊢ ( 3 = 1 ↔ ( 2 + 1 ) = ( 0 + 1 ) )
37 2cn ⊢ 2 ∈ ℂ
38 0cn ⊢ 0 ∈ ℂ
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 ∈ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ↔ ( 1 ∈ ( 1 ... 𝑁 ) ∧ 1 ≠ 3 ) )
45 33 43 44 sylanblrc ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ( ( 1 ... 𝑁 ) ∖ { 3 } ) )
46 45 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ( ( 1 ... 𝑁 ) ∖ { 3 } ) )
47 ne0i ⊢ ( 1 ∈ ( ( 1 ... 𝑁 ) ∖ { 3 } ) → ( ( 1 ... 𝑁 ) ∖ { 3 } ) ≠ ∅ )
48 rnxp ⊢ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) ≠ ∅ → ran ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) = { 0 } )
49 46 47 48 3syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ran ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) = { 0 } )
50 30 49 uneq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ran { ⟨ 3 , - 1 ⟩ } ∪ ran ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( { - 1 } ∪ { 0 } ) )
51 rnun ⊢ ran ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( ran { ⟨ 3 , - 1 ⟩ } ∪ ran ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
52 df-pr ⊢ { - 1 , 0 } = ( { - 1 } ∪ { 0 } )
53 50 51 52 3eqtr4g ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ran ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = { - 1 , 0 } )
54 ovex ⊢ ( 𝐼 + 1 ) ∈ V
55 54 rnsnop ⊢ ran { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } = { 1 }
56 55 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ran { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } = { 1 } )
57 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
58 fzssp1 ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) )
59 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
60 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
61 60 oveq2d ⊢ ( 𝑁 ∈ ℂ → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
62 59 61 syl ⊢ ( 𝑁 ∈ ℤ → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
63 58 62 sseqtrid ⊢ ( 𝑁 ∈ ℤ → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
64 57 63 syl ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
65 64 sselda ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
66 elfzelz ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℤ )
67 66 zred ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℝ )
68 id ⊢ ( 𝐼 ∈ ℝ → 𝐼 ∈ ℝ )
69 ltp1 ⊢ ( 𝐼 ∈ ℝ → 𝐼 < ( 𝐼 + 1 ) )
70 68 69 ltned ⊢ ( 𝐼 ∈ ℝ → 𝐼 ≠ ( 𝐼 + 1 ) )
71 67 70 syl ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ≠ ( 𝐼 + 1 ) )
72 71 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐼 ≠ ( 𝐼 + 1 ) )
73 eldifsn ⊢ ( 𝐼 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ↔ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐼 ≠ ( 𝐼 + 1 ) ) )
74 65 72 73 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) )
75 ne0i ⊢ ( 𝐼 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) → ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ≠ ∅ )
76 rnxp ⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ≠ ∅ → ran ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) = { 0 } )
77 74 75 76 3syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ran ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) = { 0 } )
78 56 77 uneq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ran { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ran ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) = ( { 1 } ∪ { 0 } ) )
79 rnun ⊢ ran ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) = ( ran { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ran ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
80 df-pr ⊢ { 1 , 0 } = ( { 1 } ∪ { 0 } )
81 78 79 80 3eqtr4g ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ran ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) = { 1 , 0 } )
82 53 81 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ran ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ran ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ↔ { - 1 , 0 } = { 1 , 0 } ) )
83 27 82 mtbiri ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ¬ ran ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ran ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) )
84 rneq ⊢ ( ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) → ran ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ran ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) )
85 83 84 nsyl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ¬ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) )
86 1 2 eqeq12i ⊢ ( 𝑃 = 𝑄 ↔ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) )
87 86 necon3abii ⊢ ( 𝑃 ≠ 𝑄 ↔ ¬ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) )
88 85 87 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑃 ≠ 𝑄 )