| Step | Hyp | Ref
| Expression |
| 1 | | tgcgrxfr.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | tgcgrxfr.m |
. . 3
⊢ − =
(dist‘𝐺) |
| 3 | | tgcgrxfr.r |
. . 3
⊢ ∼ =
(cgrG‘𝐺) |
| 4 | | tgcgrxfr.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | | fzo0ssnn0 13785 |
. . . . 5
⊢ (0..^4)
⊆ ℕ0 |
| 6 | | nn0ssre 12530 |
. . . . 5
⊢
ℕ0 ⊆ ℝ |
| 7 | 5, 6 | sstri 3993 |
. . . 4
⊢ (0..^4)
⊆ ℝ |
| 8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (0..^4) ⊆
ℝ) |
| 9 | | tgcgr4.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 10 | | tgcgr4.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 11 | | tgcgr4.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 12 | | tgcgr4.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 13 | 9, 10, 11, 12 | s4cld 14912 |
. . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 ∈ Word 𝑃) |
| 14 | | wrdf 14557 |
. . . . 5
⊢
(〈“𝐴𝐵𝐶𝐷”〉 ∈ Word 𝑃 → 〈“𝐴𝐵𝐶𝐷”〉:(0..^(♯‘〈“𝐴𝐵𝐶𝐷”〉))⟶𝑃) |
| 15 | 13, 14 | syl 17 |
. . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉:(0..^(♯‘〈“𝐴𝐵𝐶𝐷”〉))⟶𝑃) |
| 16 | | s4len 14938 |
. . . . . 6
⊢
(♯‘〈“𝐴𝐵𝐶𝐷”〉) = 4 |
| 17 | 16 | oveq2i 7442 |
. . . . 5
⊢
(0..^(♯‘〈“𝐴𝐵𝐶𝐷”〉)) = (0..^4) |
| 18 | 17 | feq2i 6728 |
. . . 4
⊢
(〈“𝐴𝐵𝐶𝐷”〉:(0..^(♯‘〈“𝐴𝐵𝐶𝐷”〉))⟶𝑃 ↔ 〈“𝐴𝐵𝐶𝐷”〉:(0..^4)⟶𝑃) |
| 19 | 15, 18 | sylib 218 |
. . 3
⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉:(0..^4)⟶𝑃) |
| 20 | | tgcgr4.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝑃) |
| 21 | | tgcgr4.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 22 | | tgcgr4.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| 23 | | tgcgr4.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
| 24 | 20, 21, 22, 23 | s4cld 14912 |
. . . . 5
⊢ (𝜑 → 〈“𝑊𝑋𝑌𝑍”〉 ∈ Word 𝑃) |
| 25 | | wrdf 14557 |
. . . . 5
⊢
(〈“𝑊𝑋𝑌𝑍”〉 ∈ Word 𝑃 → 〈“𝑊𝑋𝑌𝑍”〉:(0..^(♯‘〈“𝑊𝑋𝑌𝑍”〉))⟶𝑃) |
| 26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝜑 → 〈“𝑊𝑋𝑌𝑍”〉:(0..^(♯‘〈“𝑊𝑋𝑌𝑍”〉))⟶𝑃) |
| 27 | | s4len 14938 |
. . . . . 6
⊢
(♯‘〈“𝑊𝑋𝑌𝑍”〉) = 4 |
| 28 | 27 | oveq2i 7442 |
. . . . 5
⊢
(0..^(♯‘〈“𝑊𝑋𝑌𝑍”〉)) = (0..^4) |
| 29 | 28 | feq2i 6728 |
. . . 4
⊢
(〈“𝑊𝑋𝑌𝑍”〉:(0..^(♯‘〈“𝑊𝑋𝑌𝑍”〉))⟶𝑃 ↔ 〈“𝑊𝑋𝑌𝑍”〉:(0..^4)⟶𝑃) |
| 30 | 26, 29 | sylib 218 |
. . 3
⊢ (𝜑 → 〈“𝑊𝑋𝑌𝑍”〉:(0..^4)⟶𝑃) |
| 31 | 1, 2, 3, 4, 8, 19,
30 | iscgrglt 28522 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉 ∼ 〈“𝑊𝑋𝑌𝑍”〉 ↔ ∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))))) |
| 32 | 19 | fdmd 6746 |
. . . . . . 7
⊢ (𝜑 → dom 〈“𝐴𝐵𝐶𝐷”〉 = (0..^4)) |
| 33 | | 3p1e4 12411 |
. . . . . . . . 9
⊢ (3 + 1) =
4 |
| 34 | 33 | oveq2i 7442 |
. . . . . . . 8
⊢ (0..^(3 +
1)) = (0..^4) |
| 35 | | 3nn0 12544 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
| 36 | | nn0uz 12920 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
| 37 | 35, 36 | eleqtri 2839 |
. . . . . . . . 9
⊢ 3 ∈
(ℤ≥‘0) |
| 38 | | fzosplitsn 13814 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘0) → (0..^(3 + 1)) = ((0..^3) ∪
{3})) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
⊢ (0..^(3 +
1)) = ((0..^3) ∪ {3}) |
| 40 | 34, 39 | eqtr3i 2767 |
. . . . . . 7
⊢ (0..^4) =
((0..^3) ∪ {3}) |
| 41 | 32, 40 | eqtrdi 2793 |
. . . . . 6
⊢ (𝜑 → dom 〈“𝐴𝐵𝐶𝐷”〉 = ((0..^3) ∪
{3})) |
| 42 | 41 | raleqdv 3326 |
. . . . 5
⊢ (𝜑 → (∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))))) |
| 43 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑗 = 3 → (𝑖 < 𝑗 ↔ 𝑖 < 3)) |
| 44 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑗 = 3 → (〈“𝐴𝐵𝐶𝐷”〉‘𝑗) = (〈“𝐴𝐵𝐶𝐷”〉‘3)) |
| 45 | 44 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑗 = 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3))) |
| 46 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑗 = 3 → (〈“𝑊𝑋𝑌𝑍”〉‘𝑗) = (〈“𝑊𝑋𝑌𝑍”〉‘3)) |
| 47 | 46 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑗 = 3 → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) |
| 48 | 45, 47 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑗 = 3 →
(((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) ↔ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) |
| 49 | 43, 48 | imbi12d 344 |
. . . . . . 7
⊢ (𝑗 = 3 → ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 50 | 49 | ralunsn 4894 |
. . . . . 6
⊢ (3 ∈
ℕ0 → (∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 51 | 35, 50 | ax-mp 5 |
. . . . 5
⊢
(∀𝑗 ∈
((0..^3) ∪ {3})(𝑖 <
𝑗 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 52 | 42, 51 | bitrdi 287 |
. . . 4
⊢ (𝜑 → (∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 53 | 52 | ralbidv 3178 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 54 | 41 | raleqdv 3326 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
∀𝑖 ∈ ((0..^3)
∪ {3})(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 55 | | fzo0ssnn0 13785 |
. . . . . . . . . . . . . . . 16
⊢ (0..^3)
⊆ ℕ0 |
| 56 | 55, 6 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ (0..^3)
⊆ ℝ |
| 57 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ (0..^3)) |
| 58 | 56, 57 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ ℝ) |
| 59 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 = 3) |
| 60 | | 3re 12346 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ |
| 61 | 59, 60 | eqeltrdi 2849 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 ∈ ℝ) |
| 62 | | elfzolt2 13708 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0..^3) → 𝑗 < 3) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 3) |
| 64 | 63, 59 | breqtrrd 5171 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 𝑖) |
| 65 | 58, 61, 64 | ltnsymd 11410 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ¬ 𝑖 < 𝑗) |
| 66 | 65 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → (𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)))) |
| 67 | | tbtru 1548 |
. . . . . . . . . . . 12
⊢ ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ⊤)) |
| 68 | 66, 67 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ⊤)) |
| 69 | 68 | ralbidva 3176 |
. . . . . . . . . 10
⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)⊤)) |
| 70 | | 3nn 12345 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ |
| 71 | | lbfzo0 13739 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(0..^3) ↔ 3 ∈ ℕ) |
| 72 | 70, 71 | mpbir 231 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0..^3) |
| 73 | 72 | ne0ii 4344 |
. . . . . . . . . . 11
⊢ (0..^3)
≠ ∅ |
| 74 | | r19.3rzv 4499 |
. . . . . . . . . . 11
⊢ ((0..^3)
≠ ∅ → (⊤ ↔ ∀𝑗 ∈ (0..^3)⊤)) |
| 75 | 73, 74 | ax-mp 5 |
. . . . . . . . . 10
⊢ (⊤
↔ ∀𝑗 ∈
(0..^3)⊤) |
| 76 | 69, 75 | bitr4di 289 |
. . . . . . . . 9
⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ⊤)) |
| 77 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑖 = 3 → (𝑖 < 3 ↔ 3 < 3)) |
| 78 | 60 | ltnri 11370 |
. . . . . . . . . . . . 13
⊢ ¬ 3
< 3 |
| 79 | 78 | bifal 1556 |
. . . . . . . . . . . 12
⊢ (3 < 3
↔ ⊥) |
| 80 | 77, 79 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑖 = 3 → (𝑖 < 3 ↔ ⊥)) |
| 81 | 80 | imbi1d 341 |
. . . . . . . . . 10
⊢ (𝑖 = 3 → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (⊥
→ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 82 | | falim 1557 |
. . . . . . . . . . 11
⊢ (⊥
→ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) |
| 83 | 82 | bitru 1549 |
. . . . . . . . . 10
⊢ ((⊥
→ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
⊤) |
| 84 | 81, 83 | bitrdi 287 |
. . . . . . . . 9
⊢ (𝑖 = 3 → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
⊤)) |
| 85 | 76, 84 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔ (⊤
∧ ⊤))) |
| 86 | | anidm 564 |
. . . . . . . 8
⊢
((⊤ ∧ ⊤) ↔ ⊤) |
| 87 | 85, 86 | bitrdi 287 |
. . . . . . 7
⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
⊤)) |
| 88 | 87 | ralunsn 4894 |
. . . . . 6
⊢ (3 ∈
ℕ0 → (∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ∧
⊤))) |
| 89 | 35, 88 | ax-mp 5 |
. . . . 5
⊢
(∀𝑖 ∈
((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ∧
⊤)) |
| 90 | | ancom 460 |
. . . . 5
⊢
((∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ∧ ⊤)
↔ (⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 91 | | truan 1551 |
. . . . 5
⊢
((⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) ↔
∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 92 | 89, 90, 91 | 3bitri 297 |
. . . 4
⊢
(∀𝑖 ∈
((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 93 | 54, 92 | bitrdi 287 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 94 | 53, 93 | bitrd 279 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
| 95 | | r19.26 3111 |
. . 3
⊢
(∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(∀𝑖 ∈
(0..^3)∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 96 | 9, 10, 11 | s3cld 14911 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
| 97 | | wrdf 14557 |
. . . . . . . . 9
⊢
(〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 → 〈“𝐴𝐵𝐶”〉:(0..^(♯‘〈“𝐴𝐵𝐶”〉))⟶𝑃) |
| 98 | 96, 97 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉:(0..^(♯‘〈“𝐴𝐵𝐶”〉))⟶𝑃) |
| 99 | | s3len 14933 |
. . . . . . . . . 10
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
| 100 | 99 | oveq2i 7442 |
. . . . . . . . 9
⊢
(0..^(♯‘〈“𝐴𝐵𝐶”〉)) = (0..^3) |
| 101 | 100 | feq2i 6728 |
. . . . . . . 8
⊢
(〈“𝐴𝐵𝐶”〉:(0..^(♯‘〈“𝐴𝐵𝐶”〉))⟶𝑃 ↔ 〈“𝐴𝐵𝐶”〉:(0..^3)⟶𝑃) |
| 102 | 98, 101 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉:(0..^3)⟶𝑃) |
| 103 | 102 | fdmd 6746 |
. . . . . 6
⊢ (𝜑 → dom 〈“𝐴𝐵𝐶”〉 = (0..^3)) |
| 104 | 103 | raleqdv 3326 |
. . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ dom 〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
| 105 | 103, 104 | raleqbidv 3346 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
| 106 | 56 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0..^3) ⊆
ℝ) |
| 107 | 20, 21, 22 | s3cld 14911 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃) |
| 108 | | wrdf 14557 |
. . . . . . . 8
⊢
(〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃 → 〈“𝑊𝑋𝑌”〉:(0..^(♯‘〈“𝑊𝑋𝑌”〉))⟶𝑃) |
| 109 | 107, 108 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 〈“𝑊𝑋𝑌”〉:(0..^(♯‘〈“𝑊𝑋𝑌”〉))⟶𝑃) |
| 110 | | s3len 14933 |
. . . . . . . . 9
⊢
(♯‘〈“𝑊𝑋𝑌”〉) = 3 |
| 111 | 110 | oveq2i 7442 |
. . . . . . . 8
⊢
(0..^(♯‘〈“𝑊𝑋𝑌”〉)) = (0..^3) |
| 112 | 111 | feq2i 6728 |
. . . . . . 7
⊢
(〈“𝑊𝑋𝑌”〉:(0..^(♯‘〈“𝑊𝑋𝑌”〉))⟶𝑃 ↔ 〈“𝑊𝑋𝑌”〉:(0..^3)⟶𝑃) |
| 113 | 109, 112 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 〈“𝑊𝑋𝑌”〉:(0..^3)⟶𝑃) |
| 114 | 1, 2, 3, 4, 106, 102, 113 | iscgrglt 28522 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ↔ ∀𝑖 ∈ dom 〈“𝐴𝐵𝐶”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
| 115 | | df-s4 14889 |
. . . . . . . . . . 11
⊢
〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
| 116 | 115 | fveq1i 6907 |
. . . . . . . . . 10
⊢
(〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑖) |
| 117 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐴 ∈ 𝑃) |
| 118 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐵 ∈ 𝑃) |
| 119 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐶 ∈ 𝑃) |
| 120 | 117, 118,
119 | s3cld 14911 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
| 121 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐷 ∈ 𝑃) |
| 122 | 121 | s1cld 14641 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝐷”〉 ∈ Word 𝑃) |
| 123 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^3)) |
| 124 | 123, 100 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈
(0..^(♯‘〈“𝐴𝐵𝐶”〉))) |
| 125 | | ccatval1 14615 |
. . . . . . . . . . 11
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ 〈“𝐷”〉 ∈ Word 𝑃 ∧ 𝑖 ∈
(0..^(♯‘〈“𝐴𝐵𝐶”〉))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) |
| 126 | 120, 122,
124, 125 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) |
| 127 | 116, 126 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) |
| 128 | 115 | fveq1i 6907 |
. . . . . . . . . 10
⊢
(〈“𝐴𝐵𝐶𝐷”〉‘𝑗) = ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑗) |
| 129 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^3)) |
| 130 | 129, 100 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈
(0..^(♯‘〈“𝐴𝐵𝐶”〉))) |
| 131 | | ccatval1 14615 |
. . . . . . . . . . 11
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ 〈“𝐷”〉 ∈ Word 𝑃 ∧ 𝑗 ∈
(0..^(♯‘〈“𝐴𝐵𝐶”〉))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑗) = (〈“𝐴𝐵𝐶”〉‘𝑗)) |
| 132 | 120, 122,
130, 131 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑗) = (〈“𝐴𝐵𝐶”〉‘𝑗)) |
| 133 | 128, 132 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑗) = (〈“𝐴𝐵𝐶”〉‘𝑗)) |
| 134 | 127, 133 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗))) |
| 135 | | df-s4 14889 |
. . . . . . . . . . 11
⊢
〈“𝑊𝑋𝑌𝑍”〉 = (〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉) |
| 136 | 135 | fveq1i 6907 |
. . . . . . . . . 10
⊢
(〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑖) |
| 137 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑊 ∈ 𝑃) |
| 138 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑋 ∈ 𝑃) |
| 139 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑌 ∈ 𝑃) |
| 140 | 137, 138,
139 | s3cld 14911 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃) |
| 141 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑍 ∈ 𝑃) |
| 142 | 141 | s1cld 14641 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝑍”〉 ∈ Word 𝑃) |
| 143 | 123, 111 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈
(0..^(♯‘〈“𝑊𝑋𝑌”〉))) |
| 144 | | ccatval1 14615 |
. . . . . . . . . . 11
⊢
((〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃 ∧ 〈“𝑍”〉 ∈ Word 𝑃 ∧ 𝑖 ∈
(0..^(♯‘〈“𝑊𝑋𝑌”〉))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑖) = (〈“𝑊𝑋𝑌”〉‘𝑖)) |
| 145 | 140, 142,
143, 144 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑖) = (〈“𝑊𝑋𝑌”〉‘𝑖)) |
| 146 | 136, 145 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌”〉‘𝑖)) |
| 147 | 135 | fveq1i 6907 |
. . . . . . . . . 10
⊢
(〈“𝑊𝑋𝑌𝑍”〉‘𝑗) = ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑗) |
| 148 | 129, 111 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈
(0..^(♯‘〈“𝑊𝑋𝑌”〉))) |
| 149 | | ccatval1 14615 |
. . . . . . . . . . 11
⊢
((〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃 ∧ 〈“𝑍”〉 ∈ Word 𝑃 ∧ 𝑗 ∈
(0..^(♯‘〈“𝑊𝑋𝑌”〉))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑗) = (〈“𝑊𝑋𝑌”〉‘𝑗)) |
| 150 | 140, 142,
148, 149 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑗) = (〈“𝑊𝑋𝑌”〉‘𝑗)) |
| 151 | 147, 150 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑗) = (〈“𝑊𝑋𝑌”〉‘𝑗)) |
| 152 | 146, 151 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) |
| 153 | 134, 152 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) →
(((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) ↔ ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗)))) |
| 154 | 153 | imbi2d 340 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
| 155 | 154 | 2ralbidva 3219 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
| 156 | 105, 114,
155 | 3bitr4rd 312 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉)) |
| 157 | | fzo0to3tp 13791 |
. . . . . 6
⊢ (0..^3) =
{0, 1, 2} |
| 158 | 157 | raleqi 3324 |
. . . . 5
⊢
(∀𝑖 ∈
(0..^3)(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
∀𝑖 ∈ {0, 1, 2}
(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) |
| 159 | | 3pos 12371 |
. . . . . . . . . 10
⊢ 0 <
3 |
| 160 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑖 < 3 ↔ 0 < 3)) |
| 161 | 159, 160 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑖 = 0 → 𝑖 < 3) |
| 162 | 161 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 < 3) |
| 163 | | biimt 360 |
. . . . . . . 8
⊢ (𝑖 < 3 →
(((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 164 | 162, 163 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 165 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶𝐷”〉‘0)) |
| 166 | | s4fv0 14934 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) |
| 167 | 9, 166 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) |
| 168 | 165, 167 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = 𝐴) |
| 169 | | s4fv3 14937 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
| 170 | 12, 169 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
| 171 | 170 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
| 172 | 168, 171 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) = (𝐴 − 𝐷)) |
| 173 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌𝑍”〉‘0)) |
| 174 | | s4fv0 14934 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘0) = 𝑊) |
| 175 | 20, 174 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘0) = 𝑊) |
| 176 | 173, 175 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = 𝑊) |
| 177 | | s4fv3 14937 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
| 178 | 23, 177 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
| 179 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
| 180 | 176, 179 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) = (𝑊 − 𝑍)) |
| 181 | 172, 180 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍))) |
| 182 | 164, 181 | bitr3d 281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍))) |
| 183 | | 1lt3 12439 |
. . . . . . . . . 10
⊢ 1 <
3 |
| 184 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → (𝑖 < 3 ↔ 1 < 3)) |
| 185 | 183, 184 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑖 = 1 → 𝑖 < 3) |
| 186 | 185 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 < 3) |
| 187 | 186, 163 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 1) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 188 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶𝐷”〉‘1)) |
| 189 | | s4fv1 14935 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) |
| 190 | 10, 189 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) |
| 191 | 188, 190 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = 𝐵) |
| 192 | 170 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
| 193 | 191, 192 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 1) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) = (𝐵 − 𝐷)) |
| 194 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌𝑍”〉‘1)) |
| 195 | | s4fv1 14935 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘1) = 𝑋) |
| 196 | 21, 195 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘1) = 𝑋) |
| 197 | 194, 196 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = 𝑋) |
| 198 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
| 199 | 197, 198 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 1) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) = (𝑋 − 𝑍)) |
| 200 | 193, 199 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 1) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍))) |
| 201 | 187, 200 | bitr3d 281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 1) → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍))) |
| 202 | | 2lt3 12438 |
. . . . . . . . . 10
⊢ 2 <
3 |
| 203 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑖 = 2 → (𝑖 < 3 ↔ 2 < 3)) |
| 204 | 202, 203 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑖 = 2 → 𝑖 < 3) |
| 205 | 204 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 < 3) |
| 206 | 205, 163 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 2) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
| 207 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 2 → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶𝐷”〉‘2)) |
| 208 | | s4fv2 14936 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) |
| 209 | 11, 208 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) |
| 210 | 207, 209 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = 𝐶) |
| 211 | 170 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
| 212 | 210, 211 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 2) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) = (𝐶 − 𝐷)) |
| 213 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 2 → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌𝑍”〉‘2)) |
| 214 | | s4fv2 14936 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘2) = 𝑌) |
| 215 | 22, 214 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘2) = 𝑌) |
| 216 | 213, 215 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = 𝑌) |
| 217 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
| 218 | 216, 217 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 2) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) = (𝑌 − 𝑍)) |
| 219 | 212, 218 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 2) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍))) |
| 220 | 206, 219 | bitr3d 281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 2) → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍))) |
| 221 | | 0red 11264 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
| 222 | | 1red 11262 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
| 223 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 224 | 223 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) |
| 225 | 182, 201,
220, 221, 222, 224 | raltpd 4781 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))) |
| 226 | 158, 225 | bitrid 283 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))) |
| 227 | 156, 226 | anbi12d 632 |
. . 3
⊢ (𝜑 → ((∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) |
| 228 | 95, 227 | bitrid 283 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) |
| 229 | 31, 94, 228 | 3bitrd 305 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉 ∼ 〈“𝑊𝑋𝑌𝑍”〉 ↔ (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) |