Step | Hyp | Ref
| Expression |
1 | | eqid 2771 |
. . . . . 6
⊢
(mulGrp‘(𝑅‘𝑥)) = (mulGrp‘(𝑅‘𝑥)) |
2 | | eqid 2771 |
. . . . . 6
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(𝑅‘𝑥)) |
3 | 1, 2 | mgpbas 18980 |
. . . . 5
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(mulGrp‘(𝑅‘𝑥))) |
4 | | prdsmgp.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
5 | | fvco2 6584 |
. . . . . . . 8
⊢ ((𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑥) = (mulGrp‘(𝑅‘𝑥))) |
6 | 4, 5 | sylan 572 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑥) = (mulGrp‘(𝑅‘𝑥))) |
7 | 6 | eqcomd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (mulGrp‘(𝑅‘𝑥)) = ((mulGrp ∘ 𝑅)‘𝑥)) |
8 | 7 | fveq2d 6500 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(mulGrp‘(𝑅‘𝑥))) = (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
9 | 3, 8 | syl5eq 2819 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(𝑅‘𝑥)) = (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
10 | 9 | ixpeq2dva 8272 |
. . 3
⊢ (𝜑 → X𝑥 ∈
𝐼 (Base‘(𝑅‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
11 | | prdsmgp.y |
. . . 4
⊢ 𝑌 = (𝑆Xs𝑅) |
12 | | prdsmgp.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑌) |
13 | | eqid 2771 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) |
14 | 12, 13 | mgpbas 18980 |
. . . . 5
⊢
(Base‘𝑌) =
(Base‘𝑀) |
15 | 14 | eqcomi 2780 |
. . . 4
⊢
(Base‘𝑀) =
(Base‘𝑌) |
16 | | prdsmgp.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
17 | | prdsmgp.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
18 | 11, 15, 16, 17, 4 | prdsbas2 16596 |
. . 3
⊢ (𝜑 → (Base‘𝑀) = X𝑥 ∈
𝐼 (Base‘(𝑅‘𝑥))) |
19 | | prdsmgp.z |
. . . 4
⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅)) |
20 | | eqid 2771 |
. . . 4
⊢
(Base‘𝑍) =
(Base‘𝑍) |
21 | | fnmgp 18976 |
. . . . 5
⊢ mulGrp Fn
V |
22 | | ssv 3874 |
. . . . . 6
⊢ ran 𝑅 ⊆ V |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ran 𝑅 ⊆ V) |
24 | | fnco 6295 |
. . . . 5
⊢ ((mulGrp
Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V) → (mulGrp ∘ 𝑅) Fn 𝐼) |
25 | 21, 4, 23, 24 | mp3an2i 1446 |
. . . 4
⊢ (𝜑 → (mulGrp ∘ 𝑅) Fn 𝐼) |
26 | 19, 20, 16, 17, 25 | prdsbas2 16596 |
. . 3
⊢ (𝜑 → (Base‘𝑍) = X𝑥 ∈
𝐼 (Base‘((mulGrp
∘ 𝑅)‘𝑥))) |
27 | 10, 18, 26 | 3eqtr4d 2817 |
. 2
⊢ (𝜑 → (Base‘𝑀) = (Base‘𝑍)) |
28 | | eqid 2771 |
. . . 4
⊢
(.r‘𝑌) = (.r‘𝑌) |
29 | 12, 28 | mgpplusg 18978 |
. . 3
⊢
(.r‘𝑌) = (+g‘𝑀) |
30 | | eqid 2771 |
. . . . . . . . 9
⊢
(mulGrp‘(𝑅‘𝑧)) = (mulGrp‘(𝑅‘𝑧)) |
31 | | eqid 2771 |
. . . . . . . . 9
⊢
(.r‘(𝑅‘𝑧)) = (.r‘(𝑅‘𝑧)) |
32 | 30, 31 | mgpplusg 18978 |
. . . . . . . 8
⊢
(.r‘(𝑅‘𝑧)) =
(+g‘(mulGrp‘(𝑅‘𝑧))) |
33 | | fvco2 6584 |
. . . . . . . . . . 11
⊢ ((𝑅 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑧) = (mulGrp‘(𝑅‘𝑧))) |
34 | 4, 33 | sylan 572 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑧) = (mulGrp‘(𝑅‘𝑧))) |
35 | 34 | eqcomd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (mulGrp‘(𝑅‘𝑧)) = ((mulGrp ∘ 𝑅)‘𝑧)) |
36 | 35 | fveq2d 6500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) →
(+g‘(mulGrp‘(𝑅‘𝑧))) = (+g‘((mulGrp ∘
𝑅)‘𝑧))) |
37 | 32, 36 | syl5eq 2819 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (.r‘(𝑅‘𝑧)) = (+g‘((mulGrp ∘
𝑅)‘𝑧))) |
38 | 37 | oveqd 6991 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧)) = ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))) |
39 | 38 | mpteq2dva 5018 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧))) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧)))) |
40 | 27, 27, 39 | mpoeq123dv 7045 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧)))) = (𝑥 ∈ (Base‘𝑍), 𝑦 ∈ (Base‘𝑍) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))))) |
41 | | fnex 6804 |
. . . . . 6
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → 𝑅 ∈ V) |
42 | 4, 17, 41 | syl2anc 576 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ V) |
43 | | fndm 6285 |
. . . . . 6
⊢ (𝑅 Fn 𝐼 → dom 𝑅 = 𝐼) |
44 | 4, 43 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝑅 = 𝐼) |
45 | 11, 16, 42, 15, 44, 28 | prdsmulr 16586 |
. . . 4
⊢ (𝜑 → (.r‘𝑌) = (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧))))) |
46 | | fnex 6804 |
. . . . . 6
⊢ (((mulGrp
∘ 𝑅) Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → (mulGrp ∘ 𝑅) ∈ V) |
47 | 25, 17, 46 | syl2anc 576 |
. . . . 5
⊢ (𝜑 → (mulGrp ∘ 𝑅) ∈ V) |
48 | | fndm 6285 |
. . . . . 6
⊢ ((mulGrp
∘ 𝑅) Fn 𝐼 → dom (mulGrp ∘
𝑅) = 𝐼) |
49 | 25, 48 | syl 17 |
. . . . 5
⊢ (𝜑 → dom (mulGrp ∘ 𝑅) = 𝐼) |
50 | | eqid 2771 |
. . . . 5
⊢
(+g‘𝑍) = (+g‘𝑍) |
51 | 19, 16, 47, 20, 49, 50 | prdsplusg 16585 |
. . . 4
⊢ (𝜑 → (+g‘𝑍) = (𝑥 ∈ (Base‘𝑍), 𝑦 ∈ (Base‘𝑍) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))))) |
52 | 40, 45, 51 | 3eqtr4d 2817 |
. . 3
⊢ (𝜑 → (.r‘𝑌) = (+g‘𝑍)) |
53 | 29, 52 | syl5eqr 2821 |
. 2
⊢ (𝜑 → (+g‘𝑀) = (+g‘𝑍)) |
54 | 27, 53 | jca 504 |
1
⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧
(+g‘𝑀) =
(+g‘𝑍))) |