| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. 2
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑆)) |
| 2 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑆)) |
| 3 | | psrgrp.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 4 | | eqid 2737 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 5 | | eqid 2737 |
. . 3
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 6 | | psrgrp.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 7 | 6 | grpmgmd 18979 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Mgm) |
| 8 | 7 | 3ad2ant1 1134 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑅 ∈ Mgm) |
| 9 | | simp2 1138 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑆)) |
| 10 | | simp3 1139 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑦 ∈ (Base‘𝑆)) |
| 11 | 3, 4, 5, 8, 9, 10 | psraddcl 21958 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆)) |
| 12 | | ovex 7464 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 13 | 12 | rabex 5339 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
| 15 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 16 | | eqid 2737 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 17 | | simpr1 1195 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑥 ∈ (Base‘𝑆)) |
| 18 | 3, 15, 16, 4, 17 | psrelbas 21954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑥:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 19 | | simpr2 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑦 ∈ (Base‘𝑆)) |
| 20 | 3, 15, 16, 4, 19 | psrelbas 21954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑦:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 21 | | simpr3 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑧 ∈ (Base‘𝑆)) |
| 22 | 3, 15, 16, 4, 21 | psrelbas 21954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑧:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 23 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑅 ∈ Grp) |
| 24 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 25 | 15, 24 | grpass 18960 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → ((𝑟(+g‘𝑅)𝑠)(+g‘𝑅)𝑡) = (𝑟(+g‘𝑅)(𝑠(+g‘𝑅)𝑡))) |
| 26 | 23, 25 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → ((𝑟(+g‘𝑅)𝑠)(+g‘𝑅)𝑡) = (𝑟(+g‘𝑅)(𝑠(+g‘𝑅)𝑡))) |
| 27 | 14, 18, 20, 22, 26 | caofass 7737 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥 ∘f
(+g‘𝑅)𝑦) ∘f
(+g‘𝑅)𝑧) = (𝑥 ∘f
(+g‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧))) |
| 28 | 3, 4, 24, 5, 17, 19 | psradd 21957 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥(+g‘𝑆)𝑦) = (𝑥 ∘f
(+g‘𝑅)𝑦)) |
| 29 | 28 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(+g‘𝑆)𝑦) ∘f
(+g‘𝑅)𝑧) = ((𝑥 ∘f
(+g‘𝑅)𝑦) ∘f
(+g‘𝑅)𝑧)) |
| 30 | 3, 4, 24, 5, 19, 21 | psradd 21957 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑦(+g‘𝑆)𝑧) = (𝑦 ∘f
(+g‘𝑅)𝑧)) |
| 31 | 30 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥 ∘f
(+g‘𝑅)(𝑦(+g‘𝑆)𝑧)) = (𝑥 ∘f
(+g‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧))) |
| 32 | 27, 29, 31 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(+g‘𝑆)𝑦) ∘f
(+g‘𝑅)𝑧) = (𝑥 ∘f
(+g‘𝑅)(𝑦(+g‘𝑆)𝑧))) |
| 33 | 11 | 3adant3r3 1185 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆)) |
| 34 | 3, 4, 24, 5, 33, 21 | psradd 21957 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(+g‘𝑆)𝑦)(+g‘𝑆)𝑧) = ((𝑥(+g‘𝑆)𝑦) ∘f
(+g‘𝑅)𝑧)) |
| 35 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑅 ∈ Mgm) |
| 36 | 3, 4, 5, 35, 19, 21 | psraddcl 21958 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑦(+g‘𝑆)𝑧) ∈ (Base‘𝑆)) |
| 37 | 3, 4, 24, 5, 17, 36 | psradd 21957 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥(+g‘𝑆)(𝑦(+g‘𝑆)𝑧)) = (𝑥 ∘f
(+g‘𝑅)(𝑦(+g‘𝑆)𝑧))) |
| 38 | 32, 34, 37 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(+g‘𝑆)𝑦)(+g‘𝑆)𝑧) = (𝑥(+g‘𝑆)(𝑦(+g‘𝑆)𝑧))) |
| 39 | | psrgrp.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 40 | | eqid 2737 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 41 | 3, 39, 6, 16, 40, 4 | psr0cl 21972 |
. 2
⊢ (𝜑 → ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ×
{(0g‘𝑅)})
∈ (Base‘𝑆)) |
| 42 | 39 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → 𝐼 ∈ 𝑉) |
| 43 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑅 ∈ Grp) |
| 44 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑆)) |
| 45 | 3, 42, 43, 16, 40, 4, 5, 44 | psr0lid 21973 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ×
{(0g‘𝑅)})(+g‘𝑆)𝑥) = 𝑥) |
| 46 | | eqid 2737 |
. . 3
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 47 | 3, 42, 43, 16, 46, 4, 44 | psrnegcl 21974 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → ((invg‘𝑅) ∘ 𝑥) ∈ (Base‘𝑆)) |
| 48 | 3, 42, 43, 16, 46, 4, 44, 40, 5 | psrlinv 21975 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → (((invg‘𝑅) ∘ 𝑥)(+g‘𝑆)𝑥) = ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ×
{(0g‘𝑅)})) |
| 49 | 1, 2, 11, 38, 41, 45, 47, 48 | isgrpd 18976 |
1
⊢ (𝜑 → 𝑆 ∈ Grp) |