Step | Hyp | Ref
| Expression |
1 | | israg.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
2 | | israg.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
3 | | israg.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
4 | 1, 2, 3 | s3cld 14595 |
. . 3
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
5 | | fveqeq2 6775 |
. . . . 5
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((♯‘𝑤) = 3 ↔
(♯‘〈“𝐴𝐵𝐶”〉) = 3)) |
6 | | fveq1 6765 |
. . . . . . 7
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘0) = (〈“𝐴𝐵𝐶”〉‘0)) |
7 | | fveq1 6765 |
. . . . . . 7
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘2) = (〈“𝐴𝐵𝐶”〉‘2)) |
8 | 6, 7 | oveq12d 7285 |
. . . . . 6
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑤‘0) − (𝑤‘2)) = ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2))) |
9 | | fveq1 6765 |
. . . . . . . . 9
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘1) = (〈“𝐴𝐵𝐶”〉‘1)) |
10 | 9 | fveq2d 6770 |
. . . . . . . 8
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑆‘(𝑤‘1)) = (𝑆‘(〈“𝐴𝐵𝐶”〉‘1))) |
11 | 10, 7 | fveq12d 6773 |
. . . . . . 7
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑆‘(𝑤‘1))‘(𝑤‘2)) = ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))) |
12 | 6, 11 | oveq12d 7285 |
. . . . . 6
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))) = ((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))) |
13 | 8, 12 | eqeq12d 2754 |
. . . . 5
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))) ↔ ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))))) |
14 | 5, 13 | anbi12d 631 |
. . . 4
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2)))) ↔
((♯‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
15 | 14 | elrab3 3624 |
. . 3
⊢
(〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 → (〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ↔
((♯‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
16 | 4, 15 | syl 17 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ↔
((♯‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
17 | | df-rag 27065 |
. . . 4
⊢ ∟G
= (𝑔 ∈ V ↦
{𝑤 ∈ Word
(Base‘𝑔) ∣
((♯‘𝑤) = 3
∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}) |
18 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
19 | 18 | fveq2d 6770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = (Base‘𝐺)) |
20 | | israg.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
21 | 19, 20 | eqtr4di 2796 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = 𝑃) |
22 | | wrdeq 14249 |
. . . . . 6
⊢
((Base‘𝑔) =
𝑃 → Word
(Base‘𝑔) = Word 𝑃) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → Word (Base‘𝑔) = Word 𝑃) |
24 | 18 | fveq2d 6770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (dist‘𝑔) = (dist‘𝐺)) |
25 | | israg.d |
. . . . . . . . 9
⊢ − =
(dist‘𝐺) |
26 | 24, 25 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (dist‘𝑔) = − ) |
27 | 26 | oveqd 7284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0) − (𝑤‘2))) |
28 | | eqidd 2739 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑤‘0) = (𝑤‘0)) |
29 | 18 | fveq2d 6770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (pInvG‘𝑔) = (pInvG‘𝐺)) |
30 | | israg.s |
. . . . . . . . . . 11
⊢ 𝑆 = (pInvG‘𝐺) |
31 | 29, 30 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (pInvG‘𝑔) = 𝑆) |
32 | 31 | fveq1d 6768 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((pInvG‘𝑔)‘(𝑤‘1)) = (𝑆‘(𝑤‘1))) |
33 | 32 | fveq1d 6768 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)) = ((𝑆‘(𝑤‘1))‘(𝑤‘2))) |
34 | 26, 28, 33 | oveq123d 7288 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2)))) |
35 | 27, 34 | eqeq12d 2754 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))) ↔ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))) |
36 | 35 | anbi2d 629 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))) ↔ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2)))))) |
37 | 23, 36 | rabeqbidv 3417 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))} = {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))}) |
38 | | israg.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
39 | 38 | elexd 3449 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ V) |
40 | 20 | fvexi 6780 |
. . . . . . 7
⊢ 𝑃 ∈ V |
41 | 40 | wrdexi 14239 |
. . . . . 6
⊢ Word
𝑃 ∈ V |
42 | 41 | rabex 5254 |
. . . . 5
⊢ {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ∈ V |
43 | 42 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))} ∈ V) |
44 | 17, 37, 39, 43 | fvmptd2 6875 |
. . 3
⊢ (𝜑 → (∟G‘𝐺) = {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))}) |
45 | 44 | eleq2d 2824 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ Word 𝑃 ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0) − (𝑤‘2)) = ((𝑤‘0) − ((𝑆‘(𝑤‘1))‘(𝑤‘2))))})) |
46 | | s3fv0 14614 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
47 | 1, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
48 | 47 | eqcomd 2744 |
. . . . 5
⊢ (𝜑 → 𝐴 = (〈“𝐴𝐵𝐶”〉‘0)) |
49 | | s3fv2 14616 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
50 | 3, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
51 | 50 | eqcomd 2744 |
. . . . 5
⊢ (𝜑 → 𝐶 = (〈“𝐴𝐵𝐶”〉‘2)) |
52 | 48, 51 | oveq12d 7285 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐶) = ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2))) |
53 | | s3fv1 14615 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
54 | 2, 53 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
55 | 54 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (〈“𝐴𝐵𝐶”〉‘1)) |
56 | 55 | fveq2d 6770 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐵) = (𝑆‘(〈“𝐴𝐵𝐶”〉‘1))) |
57 | 56, 51 | fveq12d 6773 |
. . . . 5
⊢ (𝜑 → ((𝑆‘𝐵)‘𝐶) = ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))) |
58 | 48, 57 | oveq12d 7285 |
. . . 4
⊢ (𝜑 → (𝐴 − ((𝑆‘𝐵)‘𝐶)) = ((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))) |
59 | 52, 58 | eqeq12d 2754 |
. . 3
⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)) ↔ ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))))) |
60 | | s3len 14617 |
. . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
61 | 60 | a1i 11 |
. . . 4
⊢ (𝜑 →
(♯‘〈“𝐴𝐵𝐶”〉) = 3) |
62 | 61 | biantrurd 533 |
. . 3
⊢ (𝜑 → (((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2))) ↔
((♯‘〈“𝐴𝐵𝐶”〉) = 3 ∧ ((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) = ((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
63 | 59, 62 | bitrd 278 |
. 2
⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)) ↔ ((♯‘〈“𝐴𝐵𝐶”〉) = 3 ∧
((〈“𝐴𝐵𝐶”〉‘0) − (〈“𝐴𝐵𝐶”〉‘2)) =
((〈“𝐴𝐵𝐶”〉‘0) − ((𝑆‘(〈“𝐴𝐵𝐶”〉‘1))‘(〈“𝐴𝐵𝐶”〉‘2)))))) |
64 | 16, 45, 63 | 3bitr4d 311 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)))) |