| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ Mnd) | 
| 2 |  | pwsdiagmhm.y | . . 3
⊢ 𝑌 = (𝑅 ↑s 𝐼) | 
| 3 | 2 | pwsmnd 18785 | . 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ Mnd) | 
| 4 |  | pwsdiagmhm.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑅) | 
| 5 | 4 | fvexi 6920 | . . . . . 6
⊢ 𝐵 ∈ V | 
| 6 |  | pwsdiagmhm.f | . . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) | 
| 7 | 6 | fdiagfn 8930 | . . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) | 
| 8 | 5, 7 | mpan 690 | . . . . 5
⊢ (𝐼 ∈ 𝑊 → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) | 
| 9 | 8 | adantl 481 | . . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) | 
| 10 | 2, 4 | pwsbas 17532 | . . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑m 𝐼) = (Base‘𝑌)) | 
| 11 | 10 | feq3d 6723 | . . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(𝐵 ↑m 𝐼) ↔ 𝐹:𝐵⟶(Base‘𝑌))) | 
| 12 | 9, 11 | mpbid 232 | . . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(Base‘𝑌)) | 
| 13 |  | simplr 769 | . . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ 𝑊) | 
| 14 |  | eqid 2737 | . . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 15 | 4, 14 | mndcl 18755 | . . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 16 | 15 | 3expb 1121 | . . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 17 | 16 | adantlr 715 | . . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 18 | 6 | fvdiagfn 8931 | . . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) | 
| 19 | 13, 17, 18 | syl2anc 584 | . . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) | 
| 20 | 6 | fvdiagfn 8931 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = (𝐼 × {𝑎})) | 
| 21 | 6 | fvdiagfn 8931 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = (𝐼 × {𝑏})) | 
| 22 | 20, 21 | oveqan12d 7450 | . . . . . . . 8
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) ∧ (𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) | 
| 23 | 22 | anandis 678 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) | 
| 24 | 23 | adantll 714 | . . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) | 
| 25 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 26 |  | simpll 767 | . . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Mnd) | 
| 27 | 2, 4, 25 | pwsdiagel 17542 | . . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑎 ∈ 𝐵) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) | 
| 28 | 27 | adantrr 717 | . . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) | 
| 29 | 2, 4, 25 | pwsdiagel 17542 | . . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑏 ∈ 𝐵) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) | 
| 30 | 29 | adantrl 716 | . . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) | 
| 31 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) | 
| 32 | 2, 25, 26, 13, 28, 30, 14, 31 | pwsplusgval 17535 | . . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏})) = ((𝐼 × {𝑎}) ∘f
(+g‘𝑅)(𝐼 × {𝑏}))) | 
| 33 |  | id 22 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ 𝑊) | 
| 34 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑎 ∈ V | 
| 35 | 34 | a1i 11 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑎 ∈ V) | 
| 36 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑏 ∈ V | 
| 37 | 36 | a1i 11 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑏 ∈ V) | 
| 38 | 33, 35, 37 | ofc12 7727 | . . . . . . 7
⊢ (𝐼 ∈ 𝑊 → ((𝐼 × {𝑎}) ∘f
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) | 
| 39 | 38 | ad2antlr 727 | . . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎}) ∘f
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) | 
| 40 | 24, 32, 39 | 3eqtrd 2781 | . . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) | 
| 41 | 19, 40 | eqtr4d 2780 | . . . 4
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) | 
| 42 | 41 | ralrimivva 3202 | . . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) | 
| 43 |  | simpr 484 | . . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) | 
| 44 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 45 | 4, 44 | mndidcl 18762 | . . . . . 6
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ 𝐵) | 
| 46 | 45 | adantr 480 | . . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (0g‘𝑅) ∈ 𝐵) | 
| 47 | 6 | fvdiagfn 8931 | . . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ (0g‘𝑅) ∈ 𝐵) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) | 
| 48 | 43, 46, 47 | syl2anc 584 | . . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) | 
| 49 | 2, 44 | pws0g 18786 | . . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐼 × {(0g‘𝑅)}) = (0g‘𝑌)) | 
| 50 | 48, 49 | eqtrd 2777 | . . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (0g‘𝑌)) | 
| 51 | 12, 42, 50 | 3jca 1129 | . 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌))) | 
| 52 |  | eqid 2737 | . . 3
⊢
(0g‘𝑌) = (0g‘𝑌) | 
| 53 | 4, 25, 14, 31, 44, 52 | ismhm 18798 | . 2
⊢ (𝐹 ∈ (𝑅 MndHom 𝑌) ↔ ((𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌)))) | 
| 54 | 1, 3, 51, 53 | syl21anbrc 1345 | 1
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) |