| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → 𝑇:(0..^𝑛)⟶𝑃) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝑇:(0..^𝑛)⟶𝑃) |
| 3 | | simprl 771 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝑎 ∈ dom (𝐹 ∘ 𝑇)) |
| 4 | | ismot.p |
. . . . . . . . . . . . . 14
⊢ 𝑃 = (Base‘𝐺) |
| 5 | | ismot.m |
. . . . . . . . . . . . . 14
⊢ − =
(dist‘𝐺) |
| 6 | | motgrp.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
| 7 | | motcgrg.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) |
| 8 | 4, 5, 6, 7 | motf1o 28546 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑃) |
| 9 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑃–1-1-onto→𝑃 → 𝐹:𝑃⟶𝑃) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑃⟶𝑃) |
| 11 | 10 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → 𝐹:𝑃⟶𝑃) |
| 12 | | fco 6760 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑃⟶𝑃 ∧ 𝑇:(0..^𝑛)⟶𝑃) → (𝐹 ∘ 𝑇):(0..^𝑛)⟶𝑃) |
| 13 | 11, 1, 12 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → (𝐹 ∘ 𝑇):(0..^𝑛)⟶𝑃) |
| 14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → (𝐹 ∘ 𝑇):(0..^𝑛)⟶𝑃) |
| 15 | 14 | fdmd 6746 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → dom (𝐹 ∘ 𝑇) = (0..^𝑛)) |
| 16 | 3, 15 | eleqtrd 2843 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝑎 ∈ (0..^𝑛)) |
| 17 | | fvco3 7008 |
. . . . . . 7
⊢ ((𝑇:(0..^𝑛)⟶𝑃 ∧ 𝑎 ∈ (0..^𝑛)) → ((𝐹 ∘ 𝑇)‘𝑎) = (𝐹‘(𝑇‘𝑎))) |
| 18 | 2, 16, 17 | syl2anc 584 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → ((𝐹 ∘ 𝑇)‘𝑎) = (𝐹‘(𝑇‘𝑎))) |
| 19 | | simprr 773 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝑏 ∈ dom (𝐹 ∘ 𝑇)) |
| 20 | 19, 15 | eleqtrd 2843 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝑏 ∈ (0..^𝑛)) |
| 21 | | fvco3 7008 |
. . . . . . 7
⊢ ((𝑇:(0..^𝑛)⟶𝑃 ∧ 𝑏 ∈ (0..^𝑛)) → ((𝐹 ∘ 𝑇)‘𝑏) = (𝐹‘(𝑇‘𝑏))) |
| 22 | 2, 20, 21 | syl2anc 584 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → ((𝐹 ∘ 𝑇)‘𝑏) = (𝐹‘(𝑇‘𝑏))) |
| 23 | 18, 22 | oveq12d 7449 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → (((𝐹 ∘ 𝑇)‘𝑎) − ((𝐹 ∘ 𝑇)‘𝑏)) = ((𝐹‘(𝑇‘𝑎)) − (𝐹‘(𝑇‘𝑏)))) |
| 24 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → 𝐺 ∈ 𝑉) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝐺 ∈ 𝑉) |
| 26 | 2, 16 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → (𝑇‘𝑎) ∈ 𝑃) |
| 27 | 2, 20 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → (𝑇‘𝑏) ∈ 𝑃) |
| 28 | 7 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → 𝐹 ∈ (𝐺Ismt𝐺)) |
| 29 | 4, 5, 25, 26, 27, 28 | motcgr 28544 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → ((𝐹‘(𝑇‘𝑎)) − (𝐹‘(𝑇‘𝑏))) = ((𝑇‘𝑎) − (𝑇‘𝑏))) |
| 30 | 23, 29 | eqtrd 2777 |
. . . 4
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) ∧ (𝑎 ∈ dom (𝐹 ∘ 𝑇) ∧ 𝑏 ∈ dom (𝐹 ∘ 𝑇))) → (((𝐹 ∘ 𝑇)‘𝑎) − ((𝐹 ∘ 𝑇)‘𝑏)) = ((𝑇‘𝑎) − (𝑇‘𝑏))) |
| 31 | 30 | ralrimivva 3202 |
. . 3
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → ∀𝑎 ∈ dom (𝐹 ∘ 𝑇)∀𝑏 ∈ dom (𝐹 ∘ 𝑇)(((𝐹 ∘ 𝑇)‘𝑎) − ((𝐹 ∘ 𝑇)‘𝑏)) = ((𝑇‘𝑎) − (𝑇‘𝑏))) |
| 32 | | motcgrg.r |
. . . 4
⊢ ∼ =
(cgrG‘𝐺) |
| 33 | | fzo0ssnn0 13785 |
. . . . . 6
⊢
(0..^𝑛) ⊆
ℕ0 |
| 34 | | nn0ssre 12530 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
| 35 | 33, 34 | sstri 3993 |
. . . . 5
⊢
(0..^𝑛) ⊆
ℝ |
| 36 | 35 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → (0..^𝑛) ⊆ ℝ) |
| 37 | 4, 5, 32, 24, 36, 13, 1 | iscgrgd 28521 |
. . 3
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → ((𝐹 ∘ 𝑇) ∼ 𝑇 ↔ ∀𝑎 ∈ dom (𝐹 ∘ 𝑇)∀𝑏 ∈ dom (𝐹 ∘ 𝑇)(((𝐹 ∘ 𝑇)‘𝑎) − ((𝐹 ∘ 𝑇)‘𝑏)) = ((𝑇‘𝑎) − (𝑇‘𝑏)))) |
| 38 | 31, 37 | mpbird 257 |
. 2
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑇:(0..^𝑛)⟶𝑃) → (𝐹 ∘ 𝑇) ∼ 𝑇) |
| 39 | | motcgrg.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ Word 𝑃) |
| 40 | | iswrd 14554 |
. . 3
⊢ (𝑇 ∈ Word 𝑃 ↔ ∃𝑛 ∈ ℕ0 𝑇:(0..^𝑛)⟶𝑃) |
| 41 | 39, 40 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ0 𝑇:(0..^𝑛)⟶𝑃) |
| 42 | 38, 41 | r19.29a 3162 |
1
⊢ (𝜑 → (𝐹 ∘ 𝑇) ∼ 𝑇) |