Step | Hyp | Ref
| Expression |
1 | | axlowdimlem14.1 |
. . . . . . 7
⊢ 𝑄 = ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) |
2 | 1 | axlowdimlem10 25631 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁)) |
3 | | elee 25574 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑄 ∈ (𝔼‘𝑁) ↔ 𝑄:(1...𝑁)⟶ℝ)) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝑄 ∈ (𝔼‘𝑁) ↔ 𝑄:(1...𝑁)⟶ℝ)) |
5 | 2, 4 | mpbid 221 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄:(1...𝑁)⟶ℝ) |
6 | | ffn 5958 |
. . . . 5
⊢ (𝑄:(1...𝑁)⟶ℝ → 𝑄 Fn (1...𝑁)) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 Fn (1...𝑁)) |
8 | | axlowdimlem14.2 |
. . . . . . 7
⊢ 𝑅 = ({〈(𝐽 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐽 + 1)}) × {0})) |
9 | 8 | axlowdimlem10 25631 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → 𝑅 ∈ (𝔼‘𝑁)) |
10 | | elee 25574 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑅 ∈ (𝔼‘𝑁) ↔ 𝑅:(1...𝑁)⟶ℝ)) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝑅 ∈ (𝔼‘𝑁) ↔ 𝑅:(1...𝑁)⟶ℝ)) |
12 | 9, 11 | mpbid 221 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → 𝑅:(1...𝑁)⟶ℝ) |
13 | | ffn 5958 |
. . . . 5
⊢ (𝑅:(1...𝑁)⟶ℝ → 𝑅 Fn (1...𝑁)) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → 𝑅 Fn (1...𝑁)) |
15 | | eqfnfv 6219 |
. . . 4
⊢ ((𝑄 Fn (1...𝑁) ∧ 𝑅 Fn (1...𝑁)) → (𝑄 = 𝑅 ↔ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) |
16 | 7, 14, 15 | syl2an 493 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) ∧ (𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1)))) → (𝑄 = 𝑅 ↔ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) |
17 | 16 | 3impdi 1373 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝑄 = 𝑅 ↔ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) |
18 | | fznatpl1 12265 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) |
19 | 18 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) |
20 | 19 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝐼 + 1) ∈ (1...𝑁)) |
21 | | ax-1ne0 9884 |
. . . . . . . 8
⊢ 1 ≠
0 |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → 1 ≠ 0) |
23 | 1 | axlowdimlem11 25632 |
. . . . . . . 8
⊢ (𝑄‘(𝐼 + 1)) = 1 |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝑄‘(𝐼 + 1)) = 1) |
25 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ∈ ℤ) |
26 | 25 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ∈ ℂ) |
27 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (1...(𝑁 − 1)) → 𝐽 ∈ ℤ) |
28 | 27 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (1...(𝑁 − 1)) → 𝐽 ∈ ℂ) |
29 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
30 | | addcan2 10100 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐼 + 1) =
(𝐽 + 1) ↔ 𝐼 = 𝐽)) |
31 | 29, 30 | mp3an3 1405 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ) → ((𝐼 + 1) = (𝐽 + 1) ↔ 𝐼 = 𝐽)) |
32 | 26, 28, 31 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → ((𝐼 + 1) = (𝐽 + 1) ↔ 𝐼 = 𝐽)) |
33 | 32 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → ((𝐼 + 1) = (𝐽 + 1) ↔ 𝐼 = 𝐽)) |
34 | 33 | necon3bid 2826 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → ((𝐼 + 1) ≠ (𝐽 + 1) ↔ 𝐼 ≠ 𝐽)) |
35 | 34 | biimpar 501 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝐼 + 1) ≠ (𝐽 + 1)) |
36 | 8 | axlowdimlem12 25633 |
. . . . . . . 8
⊢ (((𝐼 + 1) ∈ (1...𝑁) ∧ (𝐼 + 1) ≠ (𝐽 + 1)) → (𝑅‘(𝐼 + 1)) = 0) |
37 | 20, 35, 36 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝑅‘(𝐼 + 1)) = 0) |
38 | 22, 24, 37 | 3netr4d 2859 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1))) |
39 | | df-ne 2782 |
. . . . . . . 8
⊢ ((𝑄‘𝑖) ≠ (𝑅‘𝑖) ↔ ¬ (𝑄‘𝑖) = (𝑅‘𝑖)) |
40 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑖 = (𝐼 + 1) → (𝑄‘𝑖) = (𝑄‘(𝐼 + 1))) |
41 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑖 = (𝐼 + 1) → (𝑅‘𝑖) = (𝑅‘(𝐼 + 1))) |
42 | 40, 41 | neeq12d 2843 |
. . . . . . . 8
⊢ (𝑖 = (𝐼 + 1) → ((𝑄‘𝑖) ≠ (𝑅‘𝑖) ↔ (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1)))) |
43 | 39, 42 | syl5bbr 273 |
. . . . . . 7
⊢ (𝑖 = (𝐼 + 1) → (¬ (𝑄‘𝑖) = (𝑅‘𝑖) ↔ (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1)))) |
44 | 43 | rspcev 3282 |
. . . . . 6
⊢ (((𝐼 + 1) ∈ (1...𝑁) ∧ (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1))) → ∃𝑖 ∈ (1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖)) |
45 | 20, 38, 44 | syl2anc 691 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → ∃𝑖 ∈ (1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖)) |
46 | 45 | ex 449 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝐼 ≠ 𝐽 → ∃𝑖 ∈ (1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖))) |
47 | | df-ne 2782 |
. . . 4
⊢ (𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽) |
48 | | rexnal 2978 |
. . . 4
⊢
(∃𝑖 ∈
(1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖) ↔ ¬ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖)) |
49 | 46, 47, 48 | 3imtr3g 283 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (¬ 𝐼 = 𝐽 → ¬ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) |
50 | 49 | con4d 113 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖) → 𝐼 = 𝐽)) |
51 | 17, 50 | sylbid 229 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝑄 = 𝑅 → 𝐼 = 𝐽)) |