| Step | Hyp | Ref
| Expression |
| 1 | | sylow1.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 2 | | sylow1lem.s |
. . . 4
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)} |
| 3 | | sylow1.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
| 4 | 3 | fvexi 6920 |
. . . . 5
⊢ 𝑋 ∈ V |
| 5 | 4 | pwex 5380 |
. . . 4
⊢ 𝒫
𝑋 ∈ V |
| 6 | 2, 5 | rabex2 5341 |
. . 3
⊢ 𝑆 ∈ V |
| 7 | 1, 6 | jctir 520 |
. 2
⊢ (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V)) |
| 8 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝑋) |
| 9 | | sylow1lem.a |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝐺) |
| 10 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) |
| 11 | 3, 9, 10 | grplmulf1o 19031 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1-onto→𝑋) |
| 12 | 1, 8, 11 | syl2an2r 685 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1-onto→𝑋) |
| 13 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1→𝑋) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1→𝑋) |
| 15 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
| 16 | | fveqeq2 6915 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑦 → ((♯‘𝑠) = (𝑃↑𝑁) ↔ (♯‘𝑦) = (𝑃↑𝑁))) |
| 17 | 16, 2 | elrab2 3695 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃↑𝑁))) |
| 18 | 15, 17 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃↑𝑁))) |
| 19 | 18 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝒫 𝑋) |
| 20 | 19 | elpwid 4609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ⊆ 𝑋) |
| 21 | | f1ssres 6811 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)):𝑋–1-1→𝑋 ∧ 𝑦 ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋) |
| 22 | 14, 20, 21 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋) |
| 23 | | resmpt 6055 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 24 | | f1eq1 6799 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋)) |
| 25 | 20, 23, 24 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (((𝑧 ∈ 𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋)) |
| 26 | 22, 25 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋) |
| 27 | | f1f 6804 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋 → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦⟶𝑋) |
| 28 | | frn 6743 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦⟶𝑋 → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) |
| 29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) |
| 30 | 4 | elpw2 5334 |
. . . . . . 7
⊢ (ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) |
| 31 | 29, 30 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋) |
| 32 | | f1f1orn 6859 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1→𝑋 → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1-onto→ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 33 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 34 | 33 | f1oen 9013 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)):𝑦–1-1-onto→ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 35 | 26, 32, 34 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 36 | | sylow1.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 37 | | ssfi 9213 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ 𝑦 ⊆ 𝑋) → 𝑦 ∈ Fin) |
| 38 | 36, 20, 37 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ Fin) |
| 39 | | ssfi 9213 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) |
| 40 | 36, 29, 39 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) |
| 41 | | hashen 14386 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((♯‘𝑦) = (♯‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
| 42 | 38, 40, 41 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ((♯‘𝑦) = (♯‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
| 43 | 35, 42 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (♯‘𝑦) = (♯‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))) |
| 44 | 18 | simprd 495 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (♯‘𝑦) = (𝑃↑𝑁)) |
| 45 | 43, 44 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → (♯‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) = (𝑃↑𝑁)) |
| 46 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑠 = ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) → ((♯‘𝑠) = (𝑃↑𝑁) ↔ (♯‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) = (𝑃↑𝑁))) |
| 47 | 46, 2 | elrab2 3695 |
. . . . . 6
⊢ (ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (♯‘ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) = (𝑃↑𝑁))) |
| 48 | 31, 45, 47 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆) |
| 49 | 48 | ralrimivva 3202 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆) |
| 50 | | sylow1lem.m |
. . . . 5
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 51 | 50 | fmpo 8093 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ ⊕ :(𝑋 × 𝑆)⟶𝑆) |
| 52 | 49, 51 | sylib 218 |
. . 3
⊢ (𝜑 → ⊕ :(𝑋 × 𝑆)⟶𝑆) |
| 53 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐺 ∈ Grp) |
| 54 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 55 | 3, 54 | grpidcl 18983 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
| 56 | 53, 55 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0g‘𝐺) ∈ 𝑋) |
| 57 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
| 58 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
| 59 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g‘𝐺)) |
| 60 | 59 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g‘𝐺) + 𝑧)) |
| 61 | 58, 60 | mpteq12dv 5233 |
. . . . . . . . 9
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
| 62 | 61 | rneqd 5949 |
. . . . . . . 8
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
| 63 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
| 64 | 63 | mptex 7243 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) ∈ V |
| 65 | 64 | rnex 7932 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑎 ↦
((0g‘𝐺)
+ 𝑧)) ∈ V |
| 66 | 62, 50, 65 | ovmpoa 7588 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑎 ∈ 𝑆) → ((0g‘𝐺) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
| 67 | 56, 57, 66 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0g‘𝐺) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧))) |
| 68 | 2 | ssrab3 4082 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ⊆ 𝒫 𝑋 |
| 69 | 68, 57 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝒫 𝑋) |
| 70 | 69 | elpwid 4609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ 𝑋) |
| 71 | 70 | sselda 3983 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝑋) |
| 72 | 3, 9, 54 | grplid 18985 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = 𝑧) |
| 73 | 53, 71, 72 | syl2an2r 685 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝑎) → ((0g‘𝐺) + 𝑧) = 𝑧) |
| 74 | 73 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = (𝑧 ∈ 𝑎 ↦ 𝑧)) |
| 75 | | mptresid 6069 |
. . . . . . . . 9
⊢ ( I
↾ 𝑎) = (𝑧 ∈ 𝑎 ↦ 𝑧) |
| 76 | 74, 75 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = ( I ↾ 𝑎)) |
| 77 | 76 | rneqd 5949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = ran ( I ↾ 𝑎)) |
| 78 | | rnresi 6093 |
. . . . . . 7
⊢ ran ( I
↾ 𝑎) = 𝑎 |
| 79 | 77, 78 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ran (𝑧 ∈ 𝑎 ↦ ((0g‘𝐺) + 𝑧)) = 𝑎) |
| 80 | 67, 79 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0g‘𝐺) ⊕ 𝑎) = 𝑎) |
| 81 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑐 + 𝑧) ∈ V |
| 82 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧))) |
| 83 | 81, 82 | abrexco 7264 |
. . . . . . . . 9
⊢ {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))} |
| 84 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
| 85 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑆) |
| 86 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
| 87 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → 𝑥 = 𝑐) |
| 88 | 87 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧)) |
| 89 | 86, 88 | mpteq12dv 5233 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
| 90 | 89 | rneqd 5949 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
| 91 | 63 | mptex 7243 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) ∈ V |
| 92 | 91 | rnex 7932 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) ∈ V |
| 93 | 90, 50, 92 | ovmpoa 7588 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑆) → (𝑐 ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
| 94 | 84, 85, 93 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧))) |
| 95 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) |
| 96 | 95 | rnmpt 5968 |
. . . . . . . . . . . 12
⊢ ran
(𝑧 ∈ 𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)} |
| 97 | 94, 96 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) = {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}) |
| 98 | 97 | rexeqdv 3327 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤))) |
| 99 | 98 | abbidv 2808 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)}) |
| 100 | 53 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝐺 ∈ Grp) |
| 101 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑏 ∈ 𝑋) |
| 103 | 84 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑐 ∈ 𝑋) |
| 104 | 71 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝑋) |
| 105 | 3, 9 | grpass 18960 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧))) |
| 106 | 100, 102,
103, 104, 105 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧))) |
| 107 | 106 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧)))) |
| 108 | 107 | rexbidva 3177 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧 ∈ 𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧)))) |
| 109 | 108 | abbidv 2808 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}) |
| 110 | 83, 99, 109 | 3eqtr4a 2803 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}) |
| 111 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) |
| 112 | 111 | rnmpt 5968 |
. . . . . . . 8
⊢ ran
(𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = (𝑏 + 𝑤)} |
| 113 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) |
| 114 | 113 | rnmpt 5968 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} |
| 115 | 110, 112,
114 | 3eqtr4g 2802 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
| 116 | 52 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⊕ :(𝑋 × 𝑆)⟶𝑆) |
| 117 | 116, 84, 85 | fovcdmd 7605 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) ∈ 𝑆) |
| 118 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → 𝑦 = (𝑐 ⊕ 𝑎)) |
| 119 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → 𝑥 = 𝑏) |
| 120 | 119 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧)) |
| 121 | 118, 120 | mpteq12dv 5233 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑧))) |
| 122 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤)) |
| 123 | 122 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) |
| 124 | 121, 123 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
| 125 | 124 | rneqd 5949 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
| 126 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑐 ⊕ 𝑎) ∈ V |
| 127 | 126 | mptex 7243 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) ∈ V |
| 128 | 127 | rnex 7932 |
. . . . . . . . 9
⊢ ran
(𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤)) ∈ V |
| 129 | 125, 50, 128 | ovmpoa 7588 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝑋 ∧ (𝑐 ⊕ 𝑎) ∈ 𝑆) → (𝑏 ⊕ (𝑐 ⊕ 𝑎)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
| 130 | 101, 117,
129 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑏 ⊕ (𝑐 ⊕ 𝑎)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ (𝑏 + 𝑤))) |
| 131 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐺 ∈ Grp) |
| 132 | 3, 9 | grpcl 18959 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑏 + 𝑐) ∈ 𝑋) |
| 133 | 131, 101,
84, 132 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑏 + 𝑐) ∈ 𝑋) |
| 134 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
| 135 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐)) |
| 136 | 135 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧)) |
| 137 | 134, 136 | mpteq12dv 5233 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
| 138 | 137 | rneqd 5949 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
| 139 | 63 | mptex 7243 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V |
| 140 | 139 | rnex 7932 |
. . . . . . . . 9
⊢ ran
(𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V |
| 141 | 138, 50, 140 | ovmpoa 7588 |
. . . . . . . 8
⊢ (((𝑏 + 𝑐) ∈ 𝑋 ∧ 𝑎 ∈ 𝑆) → ((𝑏 + 𝑐) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
| 142 | 133, 85, 141 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + 𝑐) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))) |
| 143 | 115, 130,
142 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))) |
| 144 | 143 | ralrimivva 3202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))) |
| 145 | 80, 144 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))) |
| 146 | 145 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))) |
| 147 | 52, 146 | jca 511 |
. 2
⊢ (𝜑 → ( ⊕ :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎 ∈ 𝑆 (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))))) |
| 148 | 3, 9, 54 | isga 19309 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎 ∈ 𝑆 (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))))) |
| 149 | 7, 147, 148 | sylanbrc 583 |
1
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) |