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 12415 |
. . . . 5
⊢ (0..^4)
⊆ ℕ0 |
6 | | nn0ssre 11173 |
. . . . 5
⊢
ℕ0 ⊆ ℝ |
7 | 5, 6 | sstri 3577 |
. . . 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 13468 |
. . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 ∈ Word 𝑃) |
14 | | wrdf 13165 |
. . . . 5
⊢
(〈“𝐴𝐵𝐶𝐷”〉 ∈ Word 𝑃 → 〈“𝐴𝐵𝐶𝐷”〉:(0..^(#‘〈“𝐴𝐵𝐶𝐷”〉))⟶𝑃) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉:(0..^(#‘〈“𝐴𝐵𝐶𝐷”〉))⟶𝑃) |
16 | | s4len 13494 |
. . . . . 6
⊢
(#‘〈“𝐴𝐵𝐶𝐷”〉) = 4 |
17 | 16 | oveq2i 6560 |
. . . . 5
⊢
(0..^(#‘〈“𝐴𝐵𝐶𝐷”〉)) = (0..^4) |
18 | 17 | feq2i 5950 |
. . . 4
⊢
(〈“𝐴𝐵𝐶𝐷”〉:(0..^(#‘〈“𝐴𝐵𝐶𝐷”〉))⟶𝑃 ↔ 〈“𝐴𝐵𝐶𝐷”〉:(0..^4)⟶𝑃) |
19 | 15, 18 | sylib 207 |
. . 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 13468 |
. . . . 5
⊢ (𝜑 → 〈“𝑊𝑋𝑌𝑍”〉 ∈ Word 𝑃) |
25 | | wrdf 13165 |
. . . . 5
⊢
(〈“𝑊𝑋𝑌𝑍”〉 ∈ Word 𝑃 → 〈“𝑊𝑋𝑌𝑍”〉:(0..^(#‘〈“𝑊𝑋𝑌𝑍”〉))⟶𝑃) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝜑 → 〈“𝑊𝑋𝑌𝑍”〉:(0..^(#‘〈“𝑊𝑋𝑌𝑍”〉))⟶𝑃) |
27 | | s4len 13494 |
. . . . . 6
⊢
(#‘〈“𝑊𝑋𝑌𝑍”〉) = 4 |
28 | 27 | oveq2i 6560 |
. . . . 5
⊢
(0..^(#‘〈“𝑊𝑋𝑌𝑍”〉)) = (0..^4) |
29 | 28 | feq2i 5950 |
. . . 4
⊢
(〈“𝑊𝑋𝑌𝑍”〉:(0..^(#‘〈“𝑊𝑋𝑌𝑍”〉))⟶𝑃 ↔ 〈“𝑊𝑋𝑌𝑍”〉:(0..^4)⟶𝑃) |
30 | 26, 29 | sylib 207 |
. . 3
⊢ (𝜑 → 〈“𝑊𝑋𝑌𝑍”〉:(0..^4)⟶𝑃) |
31 | 1, 2, 3, 4, 8, 19,
30 | iscgrglt 25209 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉 ∼ 〈“𝑊𝑋𝑌𝑍”〉 ↔ ∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))))) |
32 | | fdm 5964 |
. . . . . . . 8
⊢
(〈“𝐴𝐵𝐶𝐷”〉:(0..^4)⟶𝑃 → dom 〈“𝐴𝐵𝐶𝐷”〉 = (0..^4)) |
33 | 19, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 〈“𝐴𝐵𝐶𝐷”〉 = (0..^4)) |
34 | | 3p1e4 11030 |
. . . . . . . . 9
⊢ (3 + 1) =
4 |
35 | 34 | oveq2i 6560 |
. . . . . . . 8
⊢ (0..^(3 +
1)) = (0..^4) |
36 | | 3nn0 11187 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
37 | | nn0uz 11598 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
38 | 36, 37 | eleqtri 2686 |
. . . . . . . . 9
⊢ 3 ∈
(ℤ≥‘0) |
39 | | fzosplitsn 12442 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘0) → (0..^(3 + 1)) = ((0..^3) ∪
{3})) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (0..^(3 +
1)) = ((0..^3) ∪ {3}) |
41 | 35, 40 | eqtr3i 2634 |
. . . . . . 7
⊢ (0..^4) =
((0..^3) ∪ {3}) |
42 | 33, 41 | syl6eq 2660 |
. . . . . 6
⊢ (𝜑 → dom 〈“𝐴𝐵𝐶𝐷”〉 = ((0..^3) ∪
{3})) |
43 | 42 | raleqdv 3121 |
. . . . 5
⊢ (𝜑 → (∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))))) |
44 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑗 = 3 → (𝑖 < 𝑗 ↔ 𝑖 < 3)) |
45 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑗 = 3 → (〈“𝐴𝐵𝐶𝐷”〉‘𝑗) = (〈“𝐴𝐵𝐶𝐷”〉‘3)) |
46 | 45 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑗 = 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3))) |
47 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑗 = 3 → (〈“𝑊𝑋𝑌𝑍”〉‘𝑗) = (〈“𝑊𝑋𝑌𝑍”〉‘3)) |
48 | 47 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑗 = 3 → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) |
49 | 46, 48 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑗 = 3 →
(((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) ↔ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) |
50 | 44, 49 | imbi12d 333 |
. . . . . . 7
⊢ (𝑗 = 3 → ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
51 | 50 | ralunsn 4360 |
. . . . . 6
⊢ (3 ∈
ℕ0 → (∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
52 | 36, 51 | ax-mp 5 |
. . . . 5
⊢
(∀𝑗 ∈
((0..^3) ∪ {3})(𝑖 <
𝑗 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
53 | 43, 52 | syl6bb 275 |
. . . 4
⊢ (𝜑 → (∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
54 | 53 | ralbidv 2969 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
55 | 42 | raleqdv 3121 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
∀𝑖 ∈ ((0..^3)
∪ {3})(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
56 | | fzo0ssnn0 12415 |
. . . . . . . . . . . . . . . 16
⊢ (0..^3)
⊆ ℕ0 |
57 | 56, 6 | sstri 3577 |
. . . . . . . . . . . . . . 15
⊢ (0..^3)
⊆ ℝ |
58 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ (0..^3)) |
59 | 57, 58 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ ℝ) |
60 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 = 3) |
61 | 6, 36 | sselii 3565 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ |
62 | 60, 61 | syl6eqel 2696 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 ∈ ℝ) |
63 | | elfzolt2 12348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0..^3) → 𝑗 < 3) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 3) |
65 | 64, 60 | breqtrrd 4611 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 𝑖) |
66 | | ltnsym 10014 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑗 < 𝑖 → ¬ 𝑖 < 𝑗)) |
67 | 66 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ ℝ ∧ 𝑖 ∈ ℝ) ∧ 𝑗 < 𝑖) → ¬ 𝑖 < 𝑗) |
68 | 59, 62, 65, 67 | syl21anc 1317 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ¬ 𝑖 < 𝑗) |
69 | 68 | pm2.21d 117 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → (𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)))) |
70 | | tbtru 1485 |
. . . . . . . . . . . 12
⊢ ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ⊤)) |
71 | 69, 70 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ⊤)) |
72 | 71 | ralbidva 2968 |
. . . . . . . . . 10
⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)⊤)) |
73 | | 3nn 11063 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ |
74 | | lbfzo0 12375 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(0..^3) ↔ 3 ∈ ℕ) |
75 | 73, 74 | mpbir 220 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0..^3) |
76 | 75 | ne0ii 3882 |
. . . . . . . . . . 11
⊢ (0..^3)
≠ ∅ |
77 | | r19.3rzv 4016 |
. . . . . . . . . . 11
⊢ ((0..^3)
≠ ∅ → (⊤ ↔ ∀𝑗 ∈ (0..^3)⊤)) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . 10
⊢ (⊤
↔ ∀𝑗 ∈
(0..^3)⊤) |
79 | 72, 78 | syl6bbr 277 |
. . . . . . . . 9
⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ⊤)) |
80 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑖 = 3 → (𝑖 < 3 ↔ 3 < 3)) |
81 | 61 | ltnri 10025 |
. . . . . . . . . . . . 13
⊢ ¬ 3
< 3 |
82 | 81 | bifal 1488 |
. . . . . . . . . . . 12
⊢ (3 < 3
↔ ⊥) |
83 | 80, 82 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑖 = 3 → (𝑖 < 3 ↔ ⊥)) |
84 | 83 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑖 = 3 → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (⊥
→ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
85 | | falim 1489 |
. . . . . . . . . . 11
⊢ (⊥
→ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) |
86 | 85 | bitru 1487 |
. . . . . . . . . 10
⊢ ((⊥
→ ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
⊤) |
87 | 84, 86 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝑖 = 3 → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
⊤)) |
88 | 79, 87 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔ (⊤
∧ ⊤))) |
89 | | anidm 674 |
. . . . . . . 8
⊢
((⊤ ∧ ⊤) ↔ ⊤) |
90 | 88, 89 | syl6bb 275 |
. . . . . . 7
⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
⊤)) |
91 | 90 | ralunsn 4360 |
. . . . . 6
⊢ (3 ∈
ℕ0 → (∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ∧
⊤))) |
92 | 36, 91 | ax-mp 5 |
. . . . 5
⊢
(∀𝑖 ∈
((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ∧
⊤)) |
93 | | ancom 465 |
. . . . 5
⊢
((∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ∧ ⊤)
↔ (⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
94 | | truan 1492 |
. . . . 5
⊢
((⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) ↔
∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
95 | 92, 93, 94 | 3bitri 285 |
. . . 4
⊢
(∀𝑖 ∈
((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
96 | 55, 95 | syl6bb 275 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
97 | 54, 96 | bitrd 267 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶𝐷”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))))) |
98 | | r19.26 3046 |
. . 3
⊢
(∀𝑖 ∈
(0..^3)(∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(∀𝑖 ∈
(0..^3)∀𝑗 ∈
(0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
99 | 9, 10, 11 | s3cld 13467 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
100 | | wrdf 13165 |
. . . . . . . . 9
⊢
(〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 → 〈“𝐴𝐵𝐶”〉:(0..^(#‘〈“𝐴𝐵𝐶”〉))⟶𝑃) |
101 | 99, 100 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉:(0..^(#‘〈“𝐴𝐵𝐶”〉))⟶𝑃) |
102 | | s3len 13489 |
. . . . . . . . . 10
⊢
(#‘〈“𝐴𝐵𝐶”〉) = 3 |
103 | 102 | oveq2i 6560 |
. . . . . . . . 9
⊢
(0..^(#‘〈“𝐴𝐵𝐶”〉)) = (0..^3) |
104 | 103 | feq2i 5950 |
. . . . . . . 8
⊢
(〈“𝐴𝐵𝐶”〉:(0..^(#‘〈“𝐴𝐵𝐶”〉))⟶𝑃 ↔ 〈“𝐴𝐵𝐶”〉:(0..^3)⟶𝑃) |
105 | 101, 104 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉:(0..^3)⟶𝑃) |
106 | | fdm 5964 |
. . . . . . 7
⊢
(〈“𝐴𝐵𝐶”〉:(0..^3)⟶𝑃 → dom 〈“𝐴𝐵𝐶”〉 = (0..^3)) |
107 | 105, 106 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 〈“𝐴𝐵𝐶”〉 = (0..^3)) |
108 | | raleq 3115 |
. . . . . . 7
⊢ (dom
〈“𝐴𝐵𝐶”〉 = (0..^3) →
(∀𝑗 ∈ dom
〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
109 | 105, 106,
108 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ dom 〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
110 | 107, 109 | raleqbidv 3129 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ dom 〈“𝐴𝐵𝐶”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
111 | 57 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0..^3) ⊆
ℝ) |
112 | 20, 21, 22 | s3cld 13467 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃) |
113 | | wrdf 13165 |
. . . . . . . 8
⊢
(〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃 → 〈“𝑊𝑋𝑌”〉:(0..^(#‘〈“𝑊𝑋𝑌”〉))⟶𝑃) |
114 | 112, 113 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 〈“𝑊𝑋𝑌”〉:(0..^(#‘〈“𝑊𝑋𝑌”〉))⟶𝑃) |
115 | | s3len 13489 |
. . . . . . . . 9
⊢
(#‘〈“𝑊𝑋𝑌”〉) = 3 |
116 | 115 | oveq2i 6560 |
. . . . . . . 8
⊢
(0..^(#‘〈“𝑊𝑋𝑌”〉)) = (0..^3) |
117 | 116 | feq2i 5950 |
. . . . . . 7
⊢
(〈“𝑊𝑋𝑌”〉:(0..^(#‘〈“𝑊𝑋𝑌”〉))⟶𝑃 ↔ 〈“𝑊𝑋𝑌”〉:(0..^3)⟶𝑃) |
118 | 114, 117 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 〈“𝑊𝑋𝑌”〉:(0..^3)⟶𝑃) |
119 | 1, 2, 3, 4, 111, 105, 118 | iscgrglt 25209 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ↔ ∀𝑖 ∈ dom 〈“𝐴𝐵𝐶”〉∀𝑗 ∈ dom 〈“𝐴𝐵𝐶”〉(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
120 | | df-s4 13446 |
. . . . . . . . . . 11
⊢
〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
121 | 120 | fveq1i 6104 |
. . . . . . . . . 10
⊢
(〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑖) |
122 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐴 ∈ 𝑃) |
123 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐵 ∈ 𝑃) |
124 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐶 ∈ 𝑃) |
125 | 122, 123,
124 | s3cld 13467 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
126 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐷 ∈ 𝑃) |
127 | 126 | s1cld 13236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝐷”〉 ∈ Word 𝑃) |
128 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^3)) |
129 | 128, 103 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(#‘〈“𝐴𝐵𝐶”〉))) |
130 | | ccatval1 13214 |
. . . . . . . . . . 11
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ 〈“𝐷”〉 ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(#‘〈“𝐴𝐵𝐶”〉))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) |
131 | 125, 127,
129, 130 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) |
132 | 121, 131 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) |
133 | 120 | fveq1i 6104 |
. . . . . . . . . 10
⊢
(〈“𝐴𝐵𝐶𝐷”〉‘𝑗) = ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑗) |
134 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^3)) |
135 | 134, 103 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(#‘〈“𝐴𝐵𝐶”〉))) |
136 | | ccatval1 13214 |
. . . . . . . . . . 11
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ 〈“𝐷”〉 ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(#‘〈“𝐴𝐵𝐶”〉))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑗) = (〈“𝐴𝐵𝐶”〉‘𝑗)) |
137 | 125, 127,
135, 136 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉)‘𝑗) = (〈“𝐴𝐵𝐶”〉‘𝑗)) |
138 | 133, 137 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑗) = (〈“𝐴𝐵𝐶”〉‘𝑗)) |
139 | 132, 138 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗))) |
140 | | df-s4 13446 |
. . . . . . . . . . 11
⊢
〈“𝑊𝑋𝑌𝑍”〉 = (〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉) |
141 | 140 | fveq1i 6104 |
. . . . . . . . . 10
⊢
(〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑖) |
142 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑊 ∈ 𝑃) |
143 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑋 ∈ 𝑃) |
144 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑌 ∈ 𝑃) |
145 | 142, 143,
144 | s3cld 13467 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃) |
146 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑍 ∈ 𝑃) |
147 | 146 | s1cld 13236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 〈“𝑍”〉 ∈ Word 𝑃) |
148 | 128, 116 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(#‘〈“𝑊𝑋𝑌”〉))) |
149 | | ccatval1 13214 |
. . . . . . . . . . 11
⊢
((〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃 ∧ 〈“𝑍”〉 ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(#‘〈“𝑊𝑋𝑌”〉))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑖) = (〈“𝑊𝑋𝑌”〉‘𝑖)) |
150 | 145, 147,
148, 149 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑖) = (〈“𝑊𝑋𝑌”〉‘𝑖)) |
151 | 141, 150 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌”〉‘𝑖)) |
152 | 140 | fveq1i 6104 |
. . . . . . . . . 10
⊢
(〈“𝑊𝑋𝑌𝑍”〉‘𝑗) = ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑗) |
153 | 134, 116 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(#‘〈“𝑊𝑋𝑌”〉))) |
154 | | ccatval1 13214 |
. . . . . . . . . . 11
⊢
((〈“𝑊𝑋𝑌”〉 ∈ Word 𝑃 ∧ 〈“𝑍”〉 ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(#‘〈“𝑊𝑋𝑌”〉))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑗) = (〈“𝑊𝑋𝑌”〉‘𝑗)) |
155 | 145, 147,
153, 154 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝑊𝑋𝑌”〉 ++ 〈“𝑍”〉)‘𝑗) = (〈“𝑊𝑋𝑌”〉‘𝑗)) |
156 | 152, 155 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑗) = (〈“𝑊𝑋𝑌”〉‘𝑗)) |
157 | 151, 156 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))) |
158 | 139, 157 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) →
(((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗)) ↔ ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗)))) |
159 | 158 | imbi2d 329 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ (𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
160 | 159 | 2ralbidva 2971 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶”〉‘𝑖) − (〈“𝐴𝐵𝐶”〉‘𝑗)) = ((〈“𝑊𝑋𝑌”〉‘𝑖) − (〈“𝑊𝑋𝑌”〉‘𝑗))))) |
161 | 110, 119,
160 | 3bitr4rd 300 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ↔ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉)) |
162 | | fzo0to3tp 12421 |
. . . . . 6
⊢ (0..^3) =
{0, 1, 2} |
163 | | raleq 3115 |
. . . . . 6
⊢ ((0..^3)
= {0, 1, 2} → (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
∀𝑖 ∈ {0, 1, 2}
(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
164 | 162, 163 | mp1i 13 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔
∀𝑖 ∈ {0, 1, 2}
(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
165 | | 3pos 10991 |
. . . . . . . . . 10
⊢ 0 <
3 |
166 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑖 < 3 ↔ 0 < 3)) |
167 | 165, 166 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑖 = 0 → 𝑖 < 3) |
168 | 167 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 < 3) |
169 | | biimt 349 |
. . . . . . . 8
⊢ (𝑖 < 3 →
(((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
170 | 168, 169 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
171 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 = 0) |
172 | 171 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶𝐷”〉‘0)) |
173 | | s4fv0 13490 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) |
174 | 9, 173 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) |
175 | 174 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) |
176 | 172, 175 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = 𝐴) |
177 | | s4fv3 13493 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
178 | 12, 177 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
179 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
180 | 176, 179 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) = (𝐴 − 𝐷)) |
181 | 171 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌𝑍”〉‘0)) |
182 | | s4fv0 13490 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘0) = 𝑊) |
183 | 20, 182 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘0) = 𝑊) |
184 | 183 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝑊𝑋𝑌𝑍”〉‘0) = 𝑊) |
185 | 181, 184 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = 𝑊) |
186 | | s4fv3 13493 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
187 | 23, 186 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
188 | 187 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
189 | 185, 188 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) = (𝑊 − 𝑍)) |
190 | 180, 189 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍))) |
191 | 170, 190 | bitr3d 269 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍))) |
192 | | 1lt3 11073 |
. . . . . . . . . 10
⊢ 1 <
3 |
193 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → (𝑖 < 3 ↔ 1 < 3)) |
194 | 192, 193 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑖 = 1 → 𝑖 < 3) |
195 | 194 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 < 3) |
196 | 195, 169 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 1) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
197 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 = 1) |
198 | 197 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶𝐷”〉‘1)) |
199 | | s4fv1 13491 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) |
200 | 10, 199 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) |
201 | 200 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) |
202 | 198, 201 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = 𝐵) |
203 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
204 | 202, 203 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 1) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) = (𝐵 − 𝐷)) |
205 | 197 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌𝑍”〉‘1)) |
206 | | s4fv1 13491 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘1) = 𝑋) |
207 | 21, 206 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘1) = 𝑋) |
208 | 207 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝑊𝑋𝑌𝑍”〉‘1) = 𝑋) |
209 | 205, 208 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = 𝑋) |
210 | 187 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 1) → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
211 | 209, 210 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 1) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) = (𝑋 − 𝑍)) |
212 | 204, 211 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 1) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍))) |
213 | 196, 212 | bitr3d 269 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 1) → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍))) |
214 | | 2lt3 11072 |
. . . . . . . . . 10
⊢ 2 <
3 |
215 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑖 = 2 → (𝑖 < 3 ↔ 2 < 3)) |
216 | 214, 215 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑖 = 2 → 𝑖 < 3) |
217 | 216 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 < 3) |
218 | 217, 169 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 2) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))))) |
219 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2) |
220 | 219 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = (〈“𝐴𝐵𝐶𝐷”〉‘2)) |
221 | | s4fv2 13492 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) |
222 | 11, 221 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) |
223 | 222 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) |
224 | 220, 223 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝐴𝐵𝐶𝐷”〉‘𝑖) = 𝐶) |
225 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) |
226 | 224, 225 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 2) → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) = (𝐶 − 𝐷)) |
227 | 219 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = (〈“𝑊𝑋𝑌𝑍”〉‘2)) |
228 | | s4fv2 13492 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝑃 → (〈“𝑊𝑋𝑌𝑍”〉‘2) = 𝑌) |
229 | 22, 228 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝑊𝑋𝑌𝑍”〉‘2) = 𝑌) |
230 | 229 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝑊𝑋𝑌𝑍”〉‘2) = 𝑌) |
231 | 227, 230 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝑊𝑋𝑌𝑍”〉‘𝑖) = 𝑌) |
232 | 187 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 2) → (〈“𝑊𝑋𝑌𝑍”〉‘3) = 𝑍) |
233 | 231, 232 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 2) → ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) = (𝑌 − 𝑍)) |
234 | 226, 233 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 2) → (((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍))) |
235 | 218, 234 | bitr3d 269 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 2) → ((𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍))) |
236 | | 0red 9920 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
237 | | 1red 9934 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
238 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
239 | 238 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) |
240 | 191, 213,
235, 236, 237, 239 | raltpd 4258 |
. . . . 5
⊢ (𝜑 → (∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))) |
241 | 164, 240 | bitrd 267 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(𝑖 < 3 →
((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))) |
242 | 161, 241 | anbi12d 743 |
. . 3
⊢ (𝜑 → ((∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) |
243 | 98, 242 | syl5bb 271 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘𝑗)) = ((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘𝑗))) ∧ (𝑖 < 3 → ((〈“𝐴𝐵𝐶𝐷”〉‘𝑖) − (〈“𝐴𝐵𝐶𝐷”〉‘3)) =
((〈“𝑊𝑋𝑌𝑍”〉‘𝑖) − (〈“𝑊𝑋𝑌𝑍”〉‘3)))) ↔
(〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) |
244 | 31, 97, 243 | 3bitrd 293 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉 ∼ 〈“𝑊𝑋𝑌𝑍”〉 ↔ (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) |