| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(mulGrp‘(𝑅‘𝑥)) = (mulGrp‘(𝑅‘𝑥)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(𝑅‘𝑥)) |
| 3 | 1, 2 | mgpbas 20142 |
. . . . 5
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(mulGrp‘(𝑅‘𝑥))) |
| 4 | | prdsmgp.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
| 5 | | fvco2 7006 |
. . . . . . . 8
⊢ ((𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑥) = (mulGrp‘(𝑅‘𝑥))) |
| 6 | 4, 5 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑥) = (mulGrp‘(𝑅‘𝑥))) |
| 7 | 6 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (mulGrp‘(𝑅‘𝑥)) = ((mulGrp ∘ 𝑅)‘𝑥)) |
| 8 | 7 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(mulGrp‘(𝑅‘𝑥))) = (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
| 9 | 3, 8 | eqtrid 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(𝑅‘𝑥)) = (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
| 10 | 9 | ixpeq2dva 8952 |
. . 3
⊢ (𝜑 → X𝑥 ∈
𝐼 (Base‘(𝑅‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
| 11 | | prdsmgp.y |
. . . 4
⊢ 𝑌 = (𝑆Xs𝑅) |
| 12 | | prdsmgp.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑌) |
| 13 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 14 | 12, 13 | mgpbas 20142 |
. . . . 5
⊢
(Base‘𝑌) =
(Base‘𝑀) |
| 15 | 14 | eqcomi 2746 |
. . . 4
⊢
(Base‘𝑀) =
(Base‘𝑌) |
| 16 | | prdsmgp.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
| 17 | | prdsmgp.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 18 | 11, 15, 16, 17, 4 | prdsbas2 17514 |
. . 3
⊢ (𝜑 → (Base‘𝑀) = X𝑥 ∈
𝐼 (Base‘(𝑅‘𝑥))) |
| 19 | | prdsmgp.z |
. . . 4
⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅)) |
| 20 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 21 | | fnmgp 20139 |
. . . . 5
⊢ mulGrp Fn
V |
| 22 | | ssv 4008 |
. . . . . 6
⊢ ran 𝑅 ⊆ V |
| 23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ran 𝑅 ⊆ V) |
| 24 | | fnco 6686 |
. . . . 5
⊢ ((mulGrp
Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V) → (mulGrp ∘ 𝑅) Fn 𝐼) |
| 25 | 21, 4, 23, 24 | mp3an2i 1468 |
. . . 4
⊢ (𝜑 → (mulGrp ∘ 𝑅) Fn 𝐼) |
| 26 | 19, 20, 16, 17, 25 | prdsbas2 17514 |
. . 3
⊢ (𝜑 → (Base‘𝑍) = X𝑥 ∈
𝐼 (Base‘((mulGrp
∘ 𝑅)‘𝑥))) |
| 27 | 10, 18, 26 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → (Base‘𝑀) = (Base‘𝑍)) |
| 28 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑌) = (.r‘𝑌) |
| 29 | 12, 28 | mgpplusg 20141 |
. . 3
⊢
(.r‘𝑌) = (+g‘𝑀) |
| 30 | | eqid 2737 |
. . . . . . . . 9
⊢
(mulGrp‘(𝑅‘𝑧)) = (mulGrp‘(𝑅‘𝑧)) |
| 31 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘(𝑅‘𝑧)) = (.r‘(𝑅‘𝑧)) |
| 32 | 30, 31 | mgpplusg 20141 |
. . . . . . . 8
⊢
(.r‘(𝑅‘𝑧)) =
(+g‘(mulGrp‘(𝑅‘𝑧))) |
| 33 | | fvco2 7006 |
. . . . . . . . . . 11
⊢ ((𝑅 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑧) = (mulGrp‘(𝑅‘𝑧))) |
| 34 | 4, 33 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑧) = (mulGrp‘(𝑅‘𝑧))) |
| 35 | 34 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (mulGrp‘(𝑅‘𝑧)) = ((mulGrp ∘ 𝑅)‘𝑧)) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) →
(+g‘(mulGrp‘(𝑅‘𝑧))) = (+g‘((mulGrp ∘
𝑅)‘𝑧))) |
| 37 | 32, 36 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (.r‘(𝑅‘𝑧)) = (+g‘((mulGrp ∘
𝑅)‘𝑧))) |
| 38 | 37 | oveqd 7448 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧)) = ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))) |
| 39 | 38 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧))) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧)))) |
| 40 | 27, 27, 39 | mpoeq123dv 7508 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧)))) = (𝑥 ∈ (Base‘𝑍), 𝑦 ∈ (Base‘𝑍) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))))) |
| 41 | | fnex 7237 |
. . . . . 6
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → 𝑅 ∈ V) |
| 42 | 4, 17, 41 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ V) |
| 43 | 4 | fndmd 6673 |
. . . . 5
⊢ (𝜑 → dom 𝑅 = 𝐼) |
| 44 | 11, 16, 42, 15, 43, 28 | prdsmulr 17504 |
. . . 4
⊢ (𝜑 → (.r‘𝑌) = (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧))))) |
| 45 | | fnex 7237 |
. . . . . 6
⊢ (((mulGrp
∘ 𝑅) Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → (mulGrp ∘ 𝑅) ∈ V) |
| 46 | 25, 17, 45 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (mulGrp ∘ 𝑅) ∈ V) |
| 47 | 25 | fndmd 6673 |
. . . . 5
⊢ (𝜑 → dom (mulGrp ∘ 𝑅) = 𝐼) |
| 48 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑍) = (+g‘𝑍) |
| 49 | 19, 16, 46, 20, 47, 48 | prdsplusg 17503 |
. . . 4
⊢ (𝜑 → (+g‘𝑍) = (𝑥 ∈ (Base‘𝑍), 𝑦 ∈ (Base‘𝑍) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))))) |
| 50 | 40, 44, 49 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → (.r‘𝑌) = (+g‘𝑍)) |
| 51 | 29, 50 | eqtr3id 2791 |
. 2
⊢ (𝜑 → (+g‘𝑀) = (+g‘𝑍)) |
| 52 | 27, 51 | jca 511 |
1
⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧
(+g‘𝑀) =
(+g‘𝑍))) |