Step | Hyp | Ref
| Expression |
1 | | ecopopr.1 |
. . . . . . 7
⊢ ∼ =
{〈x, y〉 ∣ ((x ∈ (𝑆 × 𝑆) ∧
y ∈
(𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x =
〈z, w〉 ∧ y = 〈v,
u〉) ∧
(z + u) = (w + v)))} |
2 | | opabssxp 4357 |
. . . . . . 7
⊢
{〈x, y〉 ∣ ((x ∈ (𝑆 × 𝑆) ∧
y ∈
(𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x =
〈z, w〉 ∧ y = 〈v,
u〉) ∧
(z + u) = (w + v)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
3 | 1, 2 | eqsstri 2969 |
. . . . . 6
⊢ ∼
⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
4 | 3 | brel 4335 |
. . . . 5
⊢ (A ∼ B → (A
∈ (𝑆 × 𝑆) ∧
B ∈
(𝑆 × 𝑆))) |
5 | 4 | simpld 105 |
. . . 4
⊢ (A ∼ B → A ∈ (𝑆 × 𝑆)) |
6 | 3 | brel 4335 |
. . . 4
⊢ (B ∼ 𝐶 → (B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))) |
7 | 5, 6 | anim12i 321 |
. . 3
⊢
((A ∼ B ∧ B ∼ 𝐶) → (A ∈ (𝑆 × 𝑆) ∧
(B ∈
(𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))) |
8 | | 3anass 888 |
. . 3
⊢
((A ∈ (𝑆 × 𝑆) ∧
B ∈
(𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (A ∈ (𝑆 × 𝑆) ∧
(B ∈
(𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))) |
9 | 7, 8 | sylibr 137 |
. 2
⊢
((A ∼ B ∧ B ∼ 𝐶) → (A ∈ (𝑆 × 𝑆) ∧
B ∈
(𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))) |
10 | | eqid 2037 |
. . 3
⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆) |
11 | | breq1 3758 |
. . . . 5
⊢
(〈f, g〉 = A
→ (〈f, g〉 ∼ 〈ℎ, 𝑡〉 ↔ A ∼ 〈ℎ, 𝑡〉)) |
12 | 11 | anbi1d 438 |
. . . 4
⊢
(〈f, g〉 = A
→ ((〈f, g〉 ∼ 〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) ↔ (A ∼ 〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉))) |
13 | | breq1 3758 |
. . . 4
⊢
(〈f, g〉 = A
→ (〈f, g〉 ∼ 〈𝑠, 𝑟〉 ↔ A ∼ 〈𝑠, 𝑟〉)) |
14 | 12, 13 | imbi12d 223 |
. . 3
⊢
(〈f, g〉 = A
→ (((〈f, g〉 ∼ 〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → 〈f, g〉 ∼
〈𝑠, 𝑟〉) ↔ ((A ∼ 〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → A ∼ 〈𝑠, 𝑟〉))) |
15 | | breq2 3759 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = B → (A
∼
〈ℎ, 𝑡〉 ↔ A ∼ B)) |
16 | | breq1 3758 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = B → (〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉 ↔ B ∼ 〈𝑠, 𝑟〉)) |
17 | 15, 16 | anbi12d 442 |
. . . 4
⊢
(〈ℎ, 𝑡〉 = B → ((A
∼
〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) ↔ (A ∼ B ∧ B ∼ 〈𝑠, 𝑟〉))) |
18 | 17 | imbi1d 220 |
. . 3
⊢
(〈ℎ, 𝑡〉 = B → (((A
∼
〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → A ∼ 〈𝑠, 𝑟〉) ↔ ((A ∼ B ∧ B ∼ 〈𝑠, 𝑟〉) → A ∼ 〈𝑠, 𝑟〉))) |
19 | | breq2 3759 |
. . . . 5
⊢
(〈𝑠, 𝑟〉 = 𝐶 → (B ∼ 〈𝑠, 𝑟〉 ↔ B ∼ 𝐶)) |
20 | 19 | anbi2d 437 |
. . . 4
⊢
(〈𝑠, 𝑟〉 = 𝐶 → ((A ∼ B ∧ B ∼ 〈𝑠, 𝑟〉) ↔ (A ∼ B ∧ B ∼ 𝐶))) |
21 | | breq2 3759 |
. . . 4
⊢
(〈𝑠, 𝑟〉 = 𝐶 → (A ∼ 〈𝑠, 𝑟〉 ↔ A ∼ 𝐶)) |
22 | 20, 21 | imbi12d 223 |
. . 3
⊢
(〈𝑠, 𝑟〉 = 𝐶 → (((A ∼ B ∧ B ∼ 〈𝑠, 𝑟〉) → A ∼ 〈𝑠, 𝑟〉) ↔ ((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶))) |
23 | 1 | ecopoveq 6137 |
. . . . . . . 8
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈f, g〉 ∼
〈ℎ, 𝑡〉 ↔ (f + 𝑡) = (g
+ ℎ))) |
24 | 23 | 3adant3 923 |
. . . . . . 7
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈f, g〉 ∼
〈ℎ, 𝑡〉 ↔ (f + 𝑡) = (g
+ ℎ))) |
25 | 1 | ecopoveq 6137 |
. . . . . . . 8
⊢ (((ℎ ∈
𝑆 ∧ 𝑡
∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉 ↔ (ℎ + 𝑟) = (𝑡 + 𝑠))) |
26 | 25 | 3adant1 921 |
. . . . . . 7
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉 ↔ (ℎ + 𝑟) = (𝑡 + 𝑠))) |
27 | 24, 26 | anbi12d 442 |
. . . . . 6
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈f, g〉 ∼
〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) ↔ ((f + 𝑡) = (g
+ ℎ) ∧
(ℎ + 𝑟) = (𝑡 + 𝑠)))) |
28 | | oveq12 5464 |
. . . . . . 7
⊢
(((f + 𝑡) = (g
+ ℎ) ∧
(ℎ + 𝑟) = (𝑡 + 𝑠)) → ((f + 𝑡) + (ℎ + 𝑟)) = ((g
+ ℎ) + (𝑡 + 𝑠))) |
29 | | simp2l 929 |
. . . . . . . . 9
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ℎ ∈ 𝑆) |
30 | | simp2r 930 |
. . . . . . . . 9
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → 𝑡 ∈ 𝑆) |
31 | | simp1l 927 |
. . . . . . . . 9
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → f ∈ 𝑆) |
32 | | ecopopr.com |
. . . . . . . . . 10
⊢ (x + y) = (y + x) |
33 | 32 | a1i 9 |
. . . . . . . . 9
⊢
((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x + y) = (y + x)) |
34 | | ecopopr.ass |
. . . . . . . . . 10
⊢
((x + y) + z) = (x + (y + z)) |
35 | 34 | a1i 9 |
. . . . . . . . 9
⊢
((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x + y) + z) = (x + (y + z))) |
36 | | simp3r 932 |
. . . . . . . . 9
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → 𝑟 ∈ 𝑆) |
37 | | ecopopr.cl |
. . . . . . . . . 10
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x + y) ∈ 𝑆) |
38 | 37 | adantl 262 |
. . . . . . . . 9
⊢
((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) |
39 | 29, 30, 31, 33, 35, 36, 38 | caov411d 5628 |
. . . . . . . 8
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((ℎ + 𝑡) + (f + 𝑟)) = ((f
+ 𝑡) + (ℎ + 𝑟))) |
40 | | simp1r 928 |
. . . . . . . . . 10
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → g ∈ 𝑆) |
41 | | simp3l 931 |
. . . . . . . . . 10
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → 𝑠 ∈ 𝑆) |
42 | 40, 30, 29, 33, 35, 41, 38 | caov411d 5628 |
. . . . . . . . 9
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((g + 𝑡) + (ℎ + 𝑠)) = ((ℎ + 𝑡) + (g + 𝑠))) |
43 | 40, 30, 29, 33, 35, 41, 38 | caov4d 5627 |
. . . . . . . . 9
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((g + 𝑡) + (ℎ + 𝑠)) = ((g
+ ℎ) + (𝑡 + 𝑠))) |
44 | 42, 43 | eqtr3d 2071 |
. . . . . . . 8
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((ℎ + 𝑡) + (g + 𝑠)) = ((g
+ ℎ) + (𝑡 + 𝑠))) |
45 | 39, 44 | eqeq12d 2051 |
. . . . . . 7
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠)) ↔ ((f + 𝑡) + (ℎ + 𝑟)) = ((g
+ ℎ) + (𝑡 + 𝑠)))) |
46 | 28, 45 | syl5ibr 145 |
. . . . . 6
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((f + 𝑡) = (g
+ ℎ) ∧
(ℎ + 𝑟) = (𝑡 + 𝑠)) → ((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠)))) |
47 | 27, 46 | sylbid 139 |
. . . . 5
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈f, g〉 ∼
〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → ((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠)))) |
48 | | ecopopr.can |
. . . . . . . . 9
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x + y) = (x + z) → y =
z)) |
49 | 48 | 3adant3 923 |
. . . . . . . 8
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆) → ((x + y) = (x + z) → y =
z)) |
50 | | oveq2 5463 |
. . . . . . . 8
⊢ (y = z →
(x + y) = (x + z)) |
51 | 49, 50 | impbid1 130 |
. . . . . . 7
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆) → ((x + y) = (x + z) ↔ y =
z)) |
52 | 51 | adantl 262 |
. . . . . 6
⊢
((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x + y) = (x + z) ↔ y =
z)) |
53 | 37 | caovcl 5597 |
. . . . . . 7
⊢ ((ℎ ∈
𝑆 ∧ 𝑡
∈ 𝑆) → (ℎ + 𝑡) ∈ 𝑆) |
54 | 29, 30, 53 | syl2anc 391 |
. . . . . 6
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (ℎ + 𝑡) ∈ 𝑆) |
55 | 37 | caovcl 5597 |
. . . . . . 7
⊢
((f ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (f + 𝑟) ∈ 𝑆) |
56 | 31, 36, 55 | syl2anc 391 |
. . . . . 6
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (f + 𝑟) ∈ 𝑆) |
57 | 38, 40, 41 | caovcld 5596 |
. . . . . 6
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (g + 𝑠) ∈ 𝑆) |
58 | 52, 54, 56, 57 | caovcand 5605 |
. . . . 5
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠)) ↔ (f + 𝑟) = (g
+ 𝑠))) |
59 | 47, 58 | sylibd 138 |
. . . 4
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈f, g〉 ∼
〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → (f + 𝑟) = (g
+ 𝑠))) |
60 | 1 | ecopoveq 6137 |
. . . . 5
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟
∈ 𝑆)) → (〈f, g〉 ∼
〈𝑠, 𝑟〉 ↔ (f + 𝑟) = (g
+ 𝑠))) |
61 | 60 | 3adant2 922 |
. . . 4
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈f, g〉 ∼
〈𝑠, 𝑟〉 ↔ (f + 𝑟) = (g
+ 𝑠))) |
62 | 59, 61 | sylibrd 158 |
. . 3
⊢
(((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ
∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈f, g〉 ∼
〈ℎ, 𝑡〉 ∧
〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → 〈f, g〉 ∼
〈𝑠, 𝑟〉)) |
63 | 10, 14, 18, 22, 62 | 3optocl 4361 |
. 2
⊢
((A ∈ (𝑆 × 𝑆) ∧
B ∈
(𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶)) |
64 | 9, 63 | mpcom 32 |
1
⊢
((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶) |