Step | Hyp | Ref
| Expression |
1 | | sylow1.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
2 | | sylow1lem.s |
. . . 4
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} |
3 | | sylow1.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
4 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐺)
∈ V |
5 | 3, 4 | eqeltri 2684 |
. . . . 5
⊢ 𝑋 ∈ V |
6 | 5 | pwex 4774 |
. . . 4
⊢ 𝒫
𝑋 ∈ V |
7 | 2, 6 | rabex2 4742 |
. . 3
⊢ 𝑆 ∈ V |
8 | 1, 7 | jctir 559 |
. 2
⊢ (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V)) |
9 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝑋) |
10 | | sylow1lem.a |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝐺) |
11 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) |
12 | 3, 10, 11 | grplmulf1o 17312 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1-onto→𝑋) |
13 | 1, 9, 12 | syl2an2r 872 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1-onto→𝑋) |
14 | | f1of1 6049 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1→𝑋) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1→𝑋) |
16 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
17 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑦 → (#‘𝑠) = (#‘𝑦)) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑦 → ((#‘𝑠) = (𝑃↑𝑁) ↔ (#‘𝑦) = (𝑃↑𝑁))) |
19 | 18, 2 | elrab2 3333 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (#‘𝑦) = (𝑃↑𝑁))) |
20 | 16, 19 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (#‘𝑦) = (𝑃↑𝑁))) |
21 | 20 | simpld 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝒫 𝑋) |
22 | 21 | elpwid 4118 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ⊆ 𝑋) |
23 | | f1ssres 6021 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1→𝑋 ∧ 𝑦 ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋) |
24 | 15, 22, 23 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋) |
25 | | resmpt 5369 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
26 | | f1eq1 6009 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋)) |
27 | 22, 25, 26 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋)) |
28 | 24, 27 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋) |
29 | | f1f 6014 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋 → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦⟶𝑋) |
30 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦⟶𝑋 → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) |
32 | 5 | elpw2 4755 |
. . . . . . 7
⊢ (ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) |
33 | 31, 32 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋) |
34 | | f1f1orn 6061 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋 → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1-onto→ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
35 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
36 | 35 | f1oen 7862 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1-onto→ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
37 | 28, 34, 36 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
38 | | sylow1.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
39 | | ssfi 8065 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ 𝑦 ⊆ 𝑋) → 𝑦 ∈ Fin) |
40 | 38, 22, 39 | syl2an2r 872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ Fin) |
41 | | ssfi 8065 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) |
42 | 38, 31, 41 | syl2an2r 872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) |
43 | | hashen 12997 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((#‘𝑦) = (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
44 | 40, 42, 43 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ((#‘𝑦) = (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
45 | 37, 44 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (#‘𝑦) = (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
46 | 20 | simprd 478 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (#‘𝑦) = (𝑃↑𝑁)) |
47 | 45, 46 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) = (𝑃↑𝑁)) |
48 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑠 = ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → (#‘𝑠) = (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
49 | 48 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑠 = ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → ((#‘𝑠) = (𝑃↑𝑁) ↔ (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) = (𝑃↑𝑁))) |
50 | 49, 2 | elrab2 3333 |
. . . . . 6
⊢ (ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (#‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) = (𝑃↑𝑁))) |
51 | 33, 47, 50 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆) |
52 | 51 | ralrimivva 2954 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆) |
53 | | sylow1lem.m |
. . . . 5
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
54 | 53 | fmpt2 7126 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ ⊕ :(𝑋 × 𝑆)⟶𝑆) |
55 | 52, 54 | sylib 207 |
. . 3
⊢ (𝜑 → ⊕ :(𝑋 × 𝑆)⟶𝑆) |
56 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐺 ∈ Grp) |
57 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
58 | 3, 57 | grpidcl 17273 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
59 | 56, 58 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0g‘𝐺) ∈ 𝑋) |
60 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
61 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
62 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g‘𝐺)) |
63 | 62 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g‘𝐺) + 𝑧)) |
64 | 61, 63 | mpteq12dv 4663 |
. . . . . . . . 9
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
65 | 64 | rneqd 5274 |
. . . . . . . 8
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
66 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
67 | 66 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) ∈ V |
68 | 67 | rnex 6992 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑎 ↦
((0g‘𝐺)
+ 𝑧)) ∈ V |
69 | 65, 53, 68 | ovmpt2a 6689 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑎 ∈ 𝑆) → ((0g‘𝐺) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
70 | 59, 60, 69 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0g‘𝐺) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
71 | | ssrab2 3650 |
. . . . . . . . . . . . . . 15
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} ⊆ 𝒫 𝑋 |
72 | 2, 71 | eqsstri 3598 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ⊆ 𝒫 𝑋 |
73 | 72, 60 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝒫 𝑋) |
74 | 73 | elpwid 4118 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ 𝑋) |
75 | 74 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝑋) |
76 | 3, 10, 57 | grplid 17275 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = 𝑧) |
77 | 56, 75, 76 | syl2an2r 872 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝑎) → ((0g‘𝐺) + 𝑧) = 𝑧) |
78 | 77 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = (𝑧 ∈ 𝑎 ↦ 𝑧)) |
79 | | mptresid 5375 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ 𝑧) = ( I ↾ 𝑎) |
80 | 78, 79 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = ( I ↾ 𝑎)) |
81 | 80 | rneqd 5274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = ran ( I ↾ 𝑎)) |
82 | | rnresi 5398 |
. . . . . . 7
⊢ ran ( I
↾ 𝑎) = 𝑎 |
83 | 81, 82 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = 𝑎) |
84 | 70, 83 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0g‘𝐺) ⊕ 𝑎) = 𝑎) |
85 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑐 + 𝑧) ∈ V |
86 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧))) |
87 | 85, 86 | abrexco 6406 |
. . . . . . . . 9
⊢ {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))} |
88 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
89 | 60 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑆) |
90 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
91 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → 𝑥 = 𝑐) |
92 | 91 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧)) |
93 | 90, 92 | mpteq12dv 4663 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
94 | 93 | rneqd 5274 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
95 | 66 | mptex 6390 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) ∈ V |
96 | 95 | rnex 6992 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) ∈ V |
97 | 94, 53, 96 | ovmpt2a 6689 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑆) → (𝑐 ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
98 | 88, 89, 97 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
99 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) |
100 | 99 | rnmpt 5292 |
. . . . . . . . . . . 12
⊢ ran
(𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)} |
101 | 98, 100 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) = {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}) |
102 | 101 | rexeqdv 3122 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤))) |
103 | 102 | abbidv 2728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)}) |
104 | 56 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝐺 ∈ Grp) |
105 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑏 ∈ 𝑋) |
107 | 88 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑐 ∈ 𝑋) |
108 | 75 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝑋) |
109 | 3, 10 | grpass 17254 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧))) |
110 | 104, 106,
107, 108, 109 | syl13anc 1320 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧))) |
111 | 110 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧)))) |
112 | 111 | rexbidva 3031 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧 ∈ 𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧)))) |
113 | 112 | abbidv 2728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}) |
114 | 87, 103, 113 | 3eqtr4a 2670 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}) |
115 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) |
116 | 115 | rnmpt 5292 |
. . . . . . . 8
⊢ ran
(𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤)} |
117 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) |
118 | 117 | rnmpt 5292 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} |
119 | 114, 116,
118 | 3eqtr4g 2669 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
120 | 55 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⊕ :(𝑋 × 𝑆)⟶𝑆) |
121 | 120, 88, 89 | fovrnd 6704 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) ∈ 𝑆) |
122 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → 𝑦 = (𝑐 ⊕ 𝑎)) |
123 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → 𝑥 = 𝑏) |
124 | 123 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧)) |
125 | 122, 124 | mpteq12dv 4663 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑧))) |
126 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤)) |
127 | 126 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) |
128 | 125, 127 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
129 | 128 | rneqd 5274 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
130 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑐 ⊕ 𝑎) ∈ V |
131 | 130 | mptex 6390 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) ∈ V |
132 | 131 | rnex 6992 |
. . . . . . . . 9
⊢ ran
(𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) ∈ V |
133 | 129, 53, 132 | ovmpt2a 6689 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝑋 ∧ (𝑐 ⊕ 𝑎) ∈ 𝑆) → (𝑏 ⊕ (𝑐 ⊕ 𝑎)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
134 | 105, 121,
133 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑏 ⊕ (𝑐 ⊕ 𝑎)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
135 | 1 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐺 ∈ Grp) |
136 | 3, 10 | grpcl 17253 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑏 + 𝑐) ∈ 𝑋) |
137 | 135, 105,
88, 136 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑏 + 𝑐) ∈ 𝑋) |
138 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
139 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐)) |
140 | 139 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧)) |
141 | 138, 140 | mpteq12dv 4663 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
142 | 141 | rneqd 5274 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
143 | 66 | mptex 6390 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V |
144 | 143 | rnex 6992 |
. . . . . . . . 9
⊢ ran
(𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V |
145 | 142, 53, 144 | ovmpt2a 6689 |
. . . . . . . 8
⊢ (((𝑏 + 𝑐) ∈ 𝑋 ∧ 𝑎 ∈ 𝑆) → ((𝑏 + 𝑐) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
146 | 137, 89, 145 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + 𝑐) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
147 | 119, 134,
146 | 3eqtr4rd 2655 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))) |
148 | 147 | ralrimivva 2954 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))) |
149 | 84, 148 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))) |
150 | 149 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))) |
151 | 55, 150 | jca 553 |
. 2
⊢ (𝜑 → ( ⊕ :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎 ∈ 𝑆 (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))))) |
152 | 3, 10, 57 | isga 17547 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎 ∈ 𝑆 (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))))) |
153 | 8, 151, 152 | sylanbrc 695 |
1
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) |