| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pwspjmhmmgpd.m | . . 3
⊢ 𝑀 = (mulGrp‘𝑌) | 
| 2 |  | pwspjmhmmgpd.b | . . 3
⊢ 𝐵 = (Base‘𝑌) | 
| 3 | 1, 2 | mgpbas 20143 | . 2
⊢ 𝐵 = (Base‘𝑀) | 
| 4 |  | pwspjmhmmgpd.t | . . 3
⊢ 𝑇 = (mulGrp‘𝑅) | 
| 5 |  | eqid 2736 | . . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 6 | 4, 5 | mgpbas 20143 | . 2
⊢
(Base‘𝑅) =
(Base‘𝑇) | 
| 7 |  | eqid 2736 | . . 3
⊢
(.r‘𝑌) = (.r‘𝑌) | 
| 8 | 1, 7 | mgpplusg 20142 | . 2
⊢
(.r‘𝑌) = (+g‘𝑀) | 
| 9 |  | eqid 2736 | . . 3
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 10 | 4, 9 | mgpplusg 20142 | . 2
⊢
(.r‘𝑅) = (+g‘𝑇) | 
| 11 |  | eqid 2736 | . . 3
⊢
(1r‘𝑌) = (1r‘𝑌) | 
| 12 | 1, 11 | ringidval 20181 | . 2
⊢
(1r‘𝑌) = (0g‘𝑀) | 
| 13 |  | eqid 2736 | . . 3
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 14 | 4, 13 | ringidval 20181 | . 2
⊢
(1r‘𝑅) = (0g‘𝑇) | 
| 15 |  | pwspjmhmmgpd.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 16 |  | pwspjmhmmgpd.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 17 |  | pwspjmhmmgpd.y | . . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐼) | 
| 18 | 17 | pwsring 20322 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Ring) | 
| 19 | 15, 16, 18 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝑌 ∈ Ring) | 
| 20 | 1 | ringmgp 20237 | . . 3
⊢ (𝑌 ∈ Ring → 𝑀 ∈ Mnd) | 
| 21 | 19, 20 | syl 17 | . 2
⊢ (𝜑 → 𝑀 ∈ Mnd) | 
| 22 | 4 | ringmgp 20237 | . . 3
⊢ (𝑅 ∈ Ring → 𝑇 ∈ Mnd) | 
| 23 | 15, 22 | syl 17 | . 2
⊢ (𝜑 → 𝑇 ∈ Mnd) | 
| 24 | 15 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ Ring) | 
| 25 | 16 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐼 ∈ 𝑉) | 
| 26 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) | 
| 27 | 17, 5, 2, 24, 25, 26 | pwselbas 17535 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥:𝐼⟶(Base‘𝑅)) | 
| 28 |  | pwspjmhmmgpd.a | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝐼) | 
| 29 | 28 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐼) | 
| 30 | 27, 29 | ffvelcdmd 7104 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥‘𝐴) ∈ (Base‘𝑅)) | 
| 31 | 30 | fmpttd 7134 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘𝑅)) | 
| 32 | 15 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Ring) | 
| 33 | 16 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ 𝑉) | 
| 34 |  | simprl 770 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) | 
| 35 |  | simprr 772 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) | 
| 36 | 17, 2, 32, 33, 34, 35, 9, 7 | pwsmulrval 17537 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(.r‘𝑌)𝑏) = (𝑎 ∘f
(.r‘𝑅)𝑏)) | 
| 37 | 36 | fveq1d 6907 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑌)𝑏)‘𝐴) = ((𝑎 ∘f
(.r‘𝑅)𝑏)‘𝐴)) | 
| 38 | 17, 5, 2, 32, 33, 34 | pwselbas 17535 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎:𝐼⟶(Base‘𝑅)) | 
| 39 | 38 | ffnd 6736 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 Fn 𝐼) | 
| 40 | 17, 5, 2, 32, 33, 35 | pwselbas 17535 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏:𝐼⟶(Base‘𝑅)) | 
| 41 | 40 | ffnd 6736 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 Fn 𝐼) | 
| 42 |  | inidm 4226 | . . . . . 6
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 43 |  | eqidd 2737 | . . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝐴 ∈ 𝐼) → (𝑎‘𝐴) = (𝑎‘𝐴)) | 
| 44 |  | eqidd 2737 | . . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝐴 ∈ 𝐼) → (𝑏‘𝐴) = (𝑏‘𝐴)) | 
| 45 | 39, 41, 33, 33, 42, 43, 44 | ofval 7709 | . . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝐴 ∈ 𝐼) → ((𝑎 ∘f
(.r‘𝑅)𝑏)‘𝐴) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) | 
| 46 | 28, 45 | mpidan 689 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎 ∘f
(.r‘𝑅)𝑏)‘𝐴) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) | 
| 47 | 37, 46 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(.r‘𝑌)𝑏)‘𝐴) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) | 
| 48 | 2, 7 | ringcl 20248 | . . . . . 6
⊢ ((𝑌 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑌)𝑏) ∈ 𝐵) | 
| 49 | 19, 48 | syl3an1 1163 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑌)𝑏) ∈ 𝐵) | 
| 50 | 49 | 3expb 1120 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(.r‘𝑌)𝑏) ∈ 𝐵) | 
| 51 |  | fveq1 6904 | . . . . 5
⊢ (𝑥 = (𝑎(.r‘𝑌)𝑏) → (𝑥‘𝐴) = ((𝑎(.r‘𝑌)𝑏)‘𝐴)) | 
| 52 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) = (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) | 
| 53 |  | fvex 6918 | . . . . 5
⊢ ((𝑎(.r‘𝑌)𝑏)‘𝐴) ∈ V | 
| 54 | 51, 52, 53 | fvmpt 7015 | . . . 4
⊢ ((𝑎(.r‘𝑌)𝑏) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑎(.r‘𝑌)𝑏)) = ((𝑎(.r‘𝑌)𝑏)‘𝐴)) | 
| 55 | 50, 54 | syl 17 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑎(.r‘𝑌)𝑏)) = ((𝑎(.r‘𝑌)𝑏)‘𝐴)) | 
| 56 |  | fveq1 6904 | . . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥‘𝐴) = (𝑎‘𝐴)) | 
| 57 |  | fvex 6918 | . . . . . 6
⊢ (𝑎‘𝐴) ∈ V | 
| 58 | 56, 52, 57 | fvmpt 7015 | . . . . 5
⊢ (𝑎 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎) = (𝑎‘𝐴)) | 
| 59 | 34, 58 | syl 17 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎) = (𝑎‘𝐴)) | 
| 60 |  | fveq1 6904 | . . . . . 6
⊢ (𝑥 = 𝑏 → (𝑥‘𝐴) = (𝑏‘𝐴)) | 
| 61 |  | fvex 6918 | . . . . . 6
⊢ (𝑏‘𝐴) ∈ V | 
| 62 | 60, 52, 61 | fvmpt 7015 | . . . . 5
⊢ (𝑏 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏) = (𝑏‘𝐴)) | 
| 63 | 35, 62 | syl 17 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏) = (𝑏‘𝐴)) | 
| 64 | 59, 63 | oveq12d 7450 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎)(.r‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏)) = ((𝑎‘𝐴)(.r‘𝑅)(𝑏‘𝐴))) | 
| 65 | 47, 55, 64 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑎(.r‘𝑌)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑎)(.r‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑏))) | 
| 66 | 2, 11 | ringidcl 20263 | . . . 4
⊢ (𝑌 ∈ Ring →
(1r‘𝑌)
∈ 𝐵) | 
| 67 |  | fveq1 6904 | . . . . 5
⊢ (𝑥 = (1r‘𝑌) → (𝑥‘𝐴) = ((1r‘𝑌)‘𝐴)) | 
| 68 |  | fvex 6918 | . . . . 5
⊢
((1r‘𝑌)‘𝐴) ∈ V | 
| 69 | 67, 52, 68 | fvmpt 7015 | . . . 4
⊢
((1r‘𝑌) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(1r‘𝑌)) = ((1r‘𝑌)‘𝐴)) | 
| 70 | 19, 66, 69 | 3syl 18 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(1r‘𝑌)) = ((1r‘𝑌)‘𝐴)) | 
| 71 | 17, 13 | pws1 20323 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {(1r‘𝑅)}) = (1r‘𝑌)) | 
| 72 | 15, 16, 71 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐼 × {(1r‘𝑅)}) = (1r‘𝑌)) | 
| 73 | 72 | fveq1d 6907 | . . 3
⊢ (𝜑 → ((𝐼 × {(1r‘𝑅)})‘𝐴) = ((1r‘𝑌)‘𝐴)) | 
| 74 |  | fvex 6918 | . . . . 5
⊢
(1r‘𝑅) ∈ V | 
| 75 | 74 | fvconst2 7225 | . . . 4
⊢ (𝐴 ∈ 𝐼 → ((𝐼 × {(1r‘𝑅)})‘𝐴) = (1r‘𝑅)) | 
| 76 | 28, 75 | syl 17 | . . 3
⊢ (𝜑 → ((𝐼 × {(1r‘𝑅)})‘𝐴) = (1r‘𝑅)) | 
| 77 | 70, 73, 76 | 3eqtr2d 2782 | . 2
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(1r‘𝑌)) = (1r‘𝑅)) | 
| 78 | 3, 6, 8, 10, 12, 14, 21, 23, 31, 65, 77 | ismhmd 18800 | 1
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑀 MndHom 𝑇)) |