Step | Hyp | Ref
| Expression |
1 | | pwspjmhmmgpd.m |
. . 3
⊢ 𝑀 = (mulGrp‘𝑌) |
2 | | pwspjmhmmgpd.b |
. . 3
⊢ 𝐵 = (Base‘𝑌) |
3 | 1, 2 | mgpbas 19364 |
. 2
⊢ 𝐵 = (Base‘𝑀) |
4 | | pwspjmhmmgpd.t |
. . 3
⊢ 𝑇 = (mulGrp‘𝑅) |
5 | | eqid 2738 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | 4, 5 | mgpbas 19364 |
. 2
⊢
(Base‘𝑅) =
(Base‘𝑇) |
7 | | eqid 2738 |
. . 3
⊢
(.r‘𝑌) = (.r‘𝑌) |
8 | 1, 7 | mgpplusg 19362 |
. 2
⊢
(.r‘𝑌) = (+g‘𝑀) |
9 | | eqid 2738 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
10 | 4, 9 | mgpplusg 19362 |
. 2
⊢
(.r‘𝑅) = (+g‘𝑇) |
11 | | eqid 2738 |
. . 3
⊢
(1r‘𝑌) = (1r‘𝑌) |
12 | 1, 11 | ringidval 19372 |
. 2
⊢
(1r‘𝑌) = (0g‘𝑀) |
13 | | eqid 2738 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
14 | 4, 13 | ringidval 19372 |
. 2
⊢
(1r‘𝑅) = (0g‘𝑇) |
15 | | pwspjmhmmgpd.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
16 | | pwspjmhmmgpd.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
17 | | pwspjmhmmgpd.y |
. . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
18 | 17 | pwsring 19487 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Ring) |
19 | 15, 16, 18 | syl2anc 587 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Ring) |
20 | 1 | ringmgp 19422 |
. . 3
⊢ (𝑌 ∈ Ring → 𝑀 ∈ Mnd) |
21 | 19, 20 | syl 17 |
. 2
⊢ (𝜑 → 𝑀 ∈ Mnd) |
22 | 4 | ringmgp 19422 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑇 ∈ Mnd) |
23 | 15, 22 | syl 17 |
. 2
⊢ (𝜑 → 𝑇 ∈ Mnd) |
24 | 15 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ Ring) |
25 | 16 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
26 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
27 | 17, 5, 2, 24, 25, 26 | pwselbas 16865 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥:𝐼⟶(Base‘𝑅)) |
28 | | pwspjmhmmgpd.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝐼) |
29 | 28 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐼) |
30 | 27, 29 | ffvelrnd 6862 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥‘𝐴) ∈ (Base‘𝑅)) |
31 | 30 | fmpttd 6889 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘𝑅)) |
32 | 15 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Ring) |
33 | 16 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ 𝑉) |
34 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
35 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
36 | 17, 2, 32, 33, 34, 35, 9, 7 | pwsmulrval 16867 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(.r‘𝑌)𝑏) = (𝑎 ∘f
(.r‘𝑅)𝑏)) |
37 | 36 | fveq1d 6676 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑌)𝑏)‘𝐴) = ((𝑎 ∘f
(.r‘𝑅)𝑏)‘𝐴)) |
38 | 17, 5, 2, 32, 33, 34 | pwselbas 16865 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎:𝐼⟶(Base‘𝑅)) |
39 | 38 | ffnd 6505 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 Fn 𝐼) |
40 | 17, 5, 2, 32, 33, 35 | pwselbas 16865 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏:𝐼⟶(Base‘𝑅)) |
41 | 40 | ffnd 6505 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 Fn 𝐼) |
42 | | inidm 4109 |
. . . . . 6
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
43 | | eqidd 2739 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝐴 ∈ 𝐼) → (𝑎‘𝐴) = (𝑎‘𝐴)) |
44 | | eqidd 2739 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝐴 ∈ 𝐼) → (𝑏‘𝐴) = (𝑏‘𝐴)) |
45 | 39, 41, 33, 33, 42, 43, 44 | ofval 7435 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝐴 ∈ 𝐼) → ((𝑎 ∘f
(.r‘𝑅)𝑏)‘𝐴) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) |
46 | 28, 45 | mpidan 689 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎 ∘f
(.r‘𝑅)𝑏)‘𝐴) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) |
47 | 37, 46 | eqtrd 2773 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑌)𝑏)‘𝐴) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) |
48 | 2, 7 | ringcl 19433 |
. . . . . 6
⊢ ((𝑌 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑌)𝑏) ∈ 𝐵) |
49 | 19, 48 | syl3an1 1164 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑌)𝑏) ∈ 𝐵) |
50 | 49 | 3expb 1121 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(.r‘𝑌)𝑏) ∈ 𝐵) |
51 | | fveq1 6673 |
. . . . 5
⊢ (𝑥 = (𝑎(.r‘𝑌)𝑏) → (𝑥‘𝐴) = ((𝑎(.r‘𝑌)𝑏)‘𝐴)) |
52 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) = (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) |
53 | | fvex 6687 |
. . . . 5
⊢ ((𝑎(.r‘𝑌)𝑏)‘𝐴) ∈ V |
54 | 51, 52, 53 | fvmpt 6775 |
. . . 4
⊢ ((𝑎(.r‘𝑌)𝑏) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑎(.r‘𝑌)𝑏)) = ((𝑎(.r‘𝑌)𝑏)‘𝐴)) |
55 | 50, 54 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑎(.r‘𝑌)𝑏)) = ((𝑎(.r‘𝑌)𝑏)‘𝐴)) |
56 | | fveq1 6673 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥‘𝐴) = (𝑎‘𝐴)) |
57 | | fvex 6687 |
. . . . . 6
⊢ (𝑎‘𝐴) ∈ V |
58 | 56, 52, 57 | fvmpt 6775 |
. . . . 5
⊢ (𝑎 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎) = (𝑎‘𝐴)) |
59 | 34, 58 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎) = (𝑎‘𝐴)) |
60 | | fveq1 6673 |
. . . . . 6
⊢ (𝑥 = 𝑏 → (𝑥‘𝐴) = (𝑏‘𝐴)) |
61 | | fvex 6687 |
. . . . . 6
⊢ (𝑏‘𝐴) ∈ V |
62 | 60, 52, 61 | fvmpt 6775 |
. . . . 5
⊢ (𝑏 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏) = (𝑏‘𝐴)) |
63 | 35, 62 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏) = (𝑏‘𝐴)) |
64 | 59, 63 | oveq12d 7188 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎)(.r‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏)) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) |
65 | 47, 55, 64 | 3eqtr4d 2783 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑎(.r‘𝑌)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎)(.r‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏))) |
66 | 2, 11 | ringidcl 19440 |
. . . 4
⊢ (𝑌 ∈ Ring →
(1r‘𝑌)
∈ 𝐵) |
67 | | fveq1 6673 |
. . . . 5
⊢ (𝑥 = (1r‘𝑌) → (𝑥‘𝐴) = ((1r‘𝑌)‘𝐴)) |
68 | | fvex 6687 |
. . . . 5
⊢
((1r‘𝑌)‘𝐴) ∈ V |
69 | 67, 52, 68 | fvmpt 6775 |
. . . 4
⊢
((1r‘𝑌) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(1r‘𝑌)) = ((1r‘𝑌)‘𝐴)) |
70 | 19, 66, 69 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(1r‘𝑌)) = ((1r‘𝑌)‘𝐴)) |
71 | 17, 13 | pws1 19488 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {(1r‘𝑅)}) = (1r‘𝑌)) |
72 | 15, 16, 71 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐼 × {(1r‘𝑅)}) = (1r‘𝑌)) |
73 | 72 | fveq1d 6676 |
. . 3
⊢ (𝜑 → ((𝐼 × {(1r‘𝑅)})‘𝐴) = ((1r‘𝑌)‘𝐴)) |
74 | | fvex 6687 |
. . . . 5
⊢
(1r‘𝑅) ∈ V |
75 | 74 | fvconst2 6976 |
. . . 4
⊢ (𝐴 ∈ 𝐼 → ((𝐼 × {(1r‘𝑅)})‘𝐴) = (1r‘𝑅)) |
76 | 28, 75 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐼 × {(1r‘𝑅)})‘𝐴) = (1r‘𝑅)) |
77 | 70, 73, 76 | 3eqtr2d 2779 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(1r‘𝑌)) = (1r‘𝑅)) |
78 | 3, 6, 8, 10, 12, 14, 21, 23, 31, 65, 77 | ismhmd 39840 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑀 MndHom 𝑇)) |