Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ Mnd) |
2 | | pwsdiagmhm.y |
. . 3
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
3 | 2 | pwsmnd 18420 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ Mnd) |
4 | | pwsdiagmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
5 | 4 | fvexi 6788 |
. . . . . 6
⊢ 𝐵 ∈ V |
6 | | pwsdiagmhm.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) |
7 | 6 | fdiagfn 8678 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) |
8 | 5, 7 | mpan 687 |
. . . . 5
⊢ (𝐼 ∈ 𝑊 → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) |
9 | 8 | adantl 482 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) |
10 | 2, 4 | pwsbas 17198 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑m 𝐼) = (Base‘𝑌)) |
11 | 10 | feq3d 6587 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(𝐵 ↑m 𝐼) ↔ 𝐹:𝐵⟶(Base‘𝑌))) |
12 | 9, 11 | mpbid 231 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(Base‘𝑌)) |
13 | | simplr 766 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
14 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
15 | 4, 14 | mndcl 18393 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
16 | 15 | 3expb 1119 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
17 | 16 | adantlr 712 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
18 | 6 | fvdiagfn 8679 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
19 | 13, 17, 18 | syl2anc 584 |
. . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
20 | 6 | fvdiagfn 8679 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = (𝐼 × {𝑎})) |
21 | 6 | fvdiagfn 8679 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = (𝐼 × {𝑏})) |
22 | 20, 21 | oveqan12d 7294 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) ∧ (𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
23 | 22 | anandis 675 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
24 | 23 | adantll 711 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
25 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) |
26 | | simpll 764 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Mnd) |
27 | 2, 4, 25 | pwsdiagel 17208 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑎 ∈ 𝐵) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) |
28 | 27 | adantrr 714 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) |
29 | 2, 4, 25 | pwsdiagel 17208 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑏 ∈ 𝐵) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) |
30 | 29 | adantrl 713 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) |
31 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
32 | 2, 25, 26, 13, 28, 30, 14, 31 | pwsplusgval 17201 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏})) = ((𝐼 × {𝑎}) ∘f
(+g‘𝑅)(𝐼 × {𝑏}))) |
33 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ 𝑊) |
34 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑎 ∈ V) |
36 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑏 ∈ V) |
38 | 33, 35, 37 | ofc12 7561 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑊 → ((𝐼 × {𝑎}) ∘f
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
39 | 38 | ad2antlr 724 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎}) ∘f
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
40 | 24, 32, 39 | 3eqtrd 2782 |
. . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
41 | 19, 40 | eqtr4d 2781 |
. . . 4
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) |
42 | 41 | ralrimivva 3123 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) |
43 | | simpr 485 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
44 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
45 | 4, 44 | mndidcl 18400 |
. . . . . 6
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ 𝐵) |
46 | 45 | adantr 481 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (0g‘𝑅) ∈ 𝐵) |
47 | 6 | fvdiagfn 8679 |
. . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ (0g‘𝑅) ∈ 𝐵) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) |
48 | 43, 46, 47 | syl2anc 584 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) |
49 | 2, 44 | pws0g 18421 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐼 × {(0g‘𝑅)}) = (0g‘𝑌)) |
50 | 48, 49 | eqtrd 2778 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (0g‘𝑌)) |
51 | 12, 42, 50 | 3jca 1127 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌))) |
52 | | eqid 2738 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
53 | 4, 25, 14, 31, 44, 52 | ismhm 18432 |
. 2
⊢ (𝐹 ∈ (𝑅 MndHom 𝑌) ↔ ((𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌)))) |
54 | 1, 3, 51, 53 | syl21anbrc 1343 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) |