Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(mulGrp‘(𝑅‘𝑥)) = (mulGrp‘(𝑅‘𝑥)) |
2 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(𝑅‘𝑥)) |
3 | 1, 2 | mgpbas 18318 |
. . . . 5
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(mulGrp‘(𝑅‘𝑥))) |
4 | | prdsmgp.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
5 | | fvco2 6183 |
. . . . . . . 8
⊢ ((𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑥) = (mulGrp‘(𝑅‘𝑥))) |
6 | 4, 5 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑥) = (mulGrp‘(𝑅‘𝑥))) |
7 | 6 | eqcomd 2616 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (mulGrp‘(𝑅‘𝑥)) = ((mulGrp ∘ 𝑅)‘𝑥)) |
8 | 7 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(mulGrp‘(𝑅‘𝑥))) = (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
9 | 3, 8 | syl5eq 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Base‘(𝑅‘𝑥)) = (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
10 | 9 | ixpeq2dva 7809 |
. . 3
⊢ (𝜑 → X𝑥 ∈
𝐼 (Base‘(𝑅‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘((mulGrp ∘ 𝑅)‘𝑥))) |
11 | | prdsmgp.y |
. . . 4
⊢ 𝑌 = (𝑆Xs𝑅) |
12 | | prdsmgp.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑌) |
13 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) |
14 | 12, 13 | mgpbas 18318 |
. . . . 5
⊢
(Base‘𝑌) =
(Base‘𝑀) |
15 | 14 | eqcomi 2619 |
. . . 4
⊢
(Base‘𝑀) =
(Base‘𝑌) |
16 | | prdsmgp.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
17 | | prdsmgp.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
18 | 11, 15, 16, 17, 4 | prdsbas2 15952 |
. . 3
⊢ (𝜑 → (Base‘𝑀) = X𝑥 ∈
𝐼 (Base‘(𝑅‘𝑥))) |
19 | | prdsmgp.z |
. . . 4
⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅)) |
20 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑍) =
(Base‘𝑍) |
21 | | fnmgp 18314 |
. . . . . 6
⊢ mulGrp Fn
V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → mulGrp Fn
V) |
23 | | ssv 3588 |
. . . . . 6
⊢ ran 𝑅 ⊆ V |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝜑 → ran 𝑅 ⊆ V) |
25 | | fnco 5913 |
. . . . 5
⊢ ((mulGrp
Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V) → (mulGrp ∘ 𝑅) Fn 𝐼) |
26 | 22, 4, 24, 25 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (mulGrp ∘ 𝑅) Fn 𝐼) |
27 | 19, 20, 16, 17, 26 | prdsbas2 15952 |
. . 3
⊢ (𝜑 → (Base‘𝑍) = X𝑥 ∈
𝐼 (Base‘((mulGrp
∘ 𝑅)‘𝑥))) |
28 | 10, 18, 27 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → (Base‘𝑀) = (Base‘𝑍)) |
29 | | eqid 2610 |
. . . 4
⊢
(.r‘𝑌) = (.r‘𝑌) |
30 | 12, 29 | mgpplusg 18316 |
. . 3
⊢
(.r‘𝑌) = (+g‘𝑀) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢
(mulGrp‘(𝑅‘𝑧)) = (mulGrp‘(𝑅‘𝑧)) |
32 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘(𝑅‘𝑧)) = (.r‘(𝑅‘𝑧)) |
33 | 31, 32 | mgpplusg 18316 |
. . . . . . . 8
⊢
(.r‘(𝑅‘𝑧)) =
(+g‘(mulGrp‘(𝑅‘𝑧))) |
34 | | fvco2 6183 |
. . . . . . . . . . 11
⊢ ((𝑅 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑧) = (mulGrp‘(𝑅‘𝑧))) |
35 | 4, 34 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((mulGrp ∘ 𝑅)‘𝑧) = (mulGrp‘(𝑅‘𝑧))) |
36 | 35 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (mulGrp‘(𝑅‘𝑧)) = ((mulGrp ∘ 𝑅)‘𝑧)) |
37 | 36 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) →
(+g‘(mulGrp‘(𝑅‘𝑧))) = (+g‘((mulGrp ∘
𝑅)‘𝑧))) |
38 | 33, 37 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (.r‘(𝑅‘𝑧)) = (+g‘((mulGrp ∘
𝑅)‘𝑧))) |
39 | 38 | oveqd 6566 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧)) = ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))) |
40 | 39 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧))) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧)))) |
41 | 28, 28, 40 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧)))) = (𝑥 ∈ (Base‘𝑍), 𝑦 ∈ (Base‘𝑍) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))))) |
42 | | fnex 6386 |
. . . . . 6
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → 𝑅 ∈ V) |
43 | 4, 17, 42 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ V) |
44 | | fndm 5904 |
. . . . . 6
⊢ (𝑅 Fn 𝐼 → dom 𝑅 = 𝐼) |
45 | 4, 44 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝑅 = 𝐼) |
46 | 11, 16, 43, 15, 45, 29 | prdsmulr 15942 |
. . . 4
⊢ (𝜑 → (.r‘𝑌) = (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(.r‘(𝑅‘𝑧))(𝑦‘𝑧))))) |
47 | | fnex 6386 |
. . . . . 6
⊢ (((mulGrp
∘ 𝑅) Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → (mulGrp ∘ 𝑅) ∈ V) |
48 | 26, 17, 47 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (mulGrp ∘ 𝑅) ∈ V) |
49 | | fndm 5904 |
. . . . . 6
⊢ ((mulGrp
∘ 𝑅) Fn 𝐼 → dom (mulGrp ∘
𝑅) = 𝐼) |
50 | 26, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → dom (mulGrp ∘ 𝑅) = 𝐼) |
51 | | eqid 2610 |
. . . . 5
⊢
(+g‘𝑍) = (+g‘𝑍) |
52 | 19, 16, 48, 20, 50, 51 | prdsplusg 15941 |
. . . 4
⊢ (𝜑 → (+g‘𝑍) = (𝑥 ∈ (Base‘𝑍), 𝑦 ∈ (Base‘𝑍) ↦ (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧)(+g‘((mulGrp ∘ 𝑅)‘𝑧))(𝑦‘𝑧))))) |
53 | 41, 46, 52 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → (.r‘𝑌) = (+g‘𝑍)) |
54 | 30, 53 | syl5eqr 2658 |
. 2
⊢ (𝜑 → (+g‘𝑀) = (+g‘𝑍)) |
55 | 28, 54 | jca 553 |
1
⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧
(+g‘𝑀) =
(+g‘𝑍))) |