Step | Hyp | Ref
| Expression |
1 | | israg.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
2 | | israg.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
3 | | israg.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
4 | 1, 2, 3 | s3cld 13617 |
. . 3
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
5 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (#‘𝑤) = (#‘〈“𝐴𝐵𝐶”〉)) |
6 | 5 | eqeq1d 2624 |
. . . . 5
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((#‘𝑤) = 3 ↔
(#‘〈“𝐴𝐵𝐶”〉) = 3)) |
7 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘0) = (〈“𝐴𝐵𝐶”〉‘0)) |
8 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘2) = (〈“𝐴𝐵𝐶”〉‘2)) |
9 | 7, 8 | oveq12d 6668 |
. . . . . 6
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑤‘0) − (𝑤‘2)) = ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2))) |
10 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘1) = (〈“𝐴𝐵𝐶”〉‘1)) |
11 | 10 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑆‘(𝑤‘1)) = (𝑆‘(〈“𝐴𝐵𝐶”〉‘1))) |
12 | 11, 8 | fveq12d 6197 |
. . . . . . 7
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑆‘(𝑤‘1))‘(𝑤‘2)) = ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))) |
13 | 7, 12 | oveq12d 6668 |
. . . . . 6
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))) = ((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))) |
14 | 9, 13 | eqeq12d 2637 |
. . . . 5
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))) ↔ ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))))) |
15 | 6, 14 | anbi12d 747 |
. . . 4
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2)))) ↔
((#‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
16 | 15 | elrab3 3364 |
. . 3
⊢
(〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 → (〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ↔
((#‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
17 | 4, 16 | syl 17 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ↔
((#‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
18 | | df-rag 25589 |
. . . . 5
⊢ ∟G
= (𝑔 ∈ V ↦
{𝑤 ∈ Word
(Base‘𝑔) ∣
((#‘𝑤) = 3 ∧
((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}) |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})) |
20 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
21 | 20 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = (Base‘𝐺)) |
22 | | israg.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
23 | 21, 22 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = 𝑃) |
24 | | wrdeq 13327 |
. . . . . 6
⊢
((Base‘𝑔) =
𝑃 → Word
(Base‘𝑔) = Word 𝑃) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → Word (Base‘𝑔) = Word 𝑃) |
26 | 20 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (dist‘𝑔) = (dist‘𝐺)) |
27 | | israg.d |
. . . . . . . . 9
⊢ − =
(dist‘𝐺) |
28 | 26, 27 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (dist‘𝑔) = − ) |
29 | 28 | oveqd 6667 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0) − (𝑤‘2))) |
30 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑤‘0) = (𝑤‘0)) |
31 | 20 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (pInvG‘𝑔) = (pInvG‘𝐺)) |
32 | | israg.s |
. . . . . . . . . . 11
⊢ 𝑆 = (pInvG‘𝐺) |
33 | 31, 32 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (pInvG‘𝑔) = 𝑆) |
34 | 33 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((pInvG‘𝑔)‘(𝑤‘1)) = (𝑆‘(𝑤‘1))) |
35 | 34 | fveq1d 6193 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)) = ((𝑆‘(𝑤‘1))‘(𝑤‘2))) |
36 | 28, 30, 35 | oveq123d 6671 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2)))) |
37 | 29, 36 | eqeq12d 2637 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))) ↔ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))) |
38 | 37 | anbi2d 740 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))) ↔ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2)))))) |
39 | 25, 38 | rabeqbidv 3195 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))} = {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))}) |
40 | | israg.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
41 | 40 | elexd 3214 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ V) |
42 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
43 | 22, 42 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑃 ∈ V |
44 | | wrdexg 13315 |
. . . . . . 7
⊢ (𝑃 ∈ V → Word 𝑃 ∈ V) |
45 | 43, 44 | ax-mp 5 |
. . . . . 6
⊢ Word
𝑃 ∈ V |
46 | 45 | rabex 4813 |
. . . . 5
⊢ {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ∈ V |
47 | 46 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ∈ V) |
48 | 19, 39, 41, 47 | fvmptd 6288 |
. . 3
⊢ (𝜑 → (∟G‘𝐺) = {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))}) |
49 | 48 | eleq2d 2687 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ Word 𝑃 ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))})) |
50 | | s3fv0 13636 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
51 | 1, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
52 | 51 | eqcomd 2628 |
. . . . 5
⊢ (𝜑 → 𝐴 = (〈“𝐴𝐵𝐶”〉‘0)) |
53 | | s3fv2 13638 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
54 | 3, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
55 | 54 | eqcomd 2628 |
. . . . 5
⊢ (𝜑 → 𝐶 = (〈“𝐴𝐵𝐶”〉‘2)) |
56 | 52, 55 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐶) = ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2))) |
57 | | s3fv1 13637 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
58 | 2, 57 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
59 | 58 | eqcomd 2628 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (〈“𝐴𝐵𝐶”〉‘1)) |
60 | 59 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐵) = (𝑆‘(〈“𝐴𝐵𝐶”〉‘1))) |
61 | 60, 55 | fveq12d 6197 |
. . . . 5
⊢ (𝜑 → ((𝑆‘𝐵)‘𝐶) = ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))) |
62 | 52, 61 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (𝐴 − ((𝑆‘𝐵)‘𝐶)) = ((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))) |
63 | 56, 62 | eqeq12d 2637 |
. . 3
⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)) ↔ ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))))) |
64 | | s3len 13639 |
. . . . 5
⊢
(#‘〈“𝐴𝐵𝐶”〉) = 3 |
65 | 64 | a1i 11 |
. . . 4
⊢ (𝜑 →
(#‘〈“𝐴𝐵𝐶”〉) = 3) |
66 | 65 | biantrurd 529 |
. . 3
⊢ (𝜑 → (((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))) ↔
((#‘〈“𝐴𝐵𝐶”〉) = 3 ∧ ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) = ((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
67 | 63, 66 | bitrd 268 |
. 2
⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)) ↔ ((#‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
68 | 17, 49, 67 | 3bitr4d 300 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)))) |