Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ Mnd) |
2 | | pwsdiagmhm.y |
. . . 4
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
3 | 2 | pwsmnd 17148 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ Mnd) |
4 | 1, 3 | jca 553 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd)) |
5 | | pwsdiagmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
6 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
7 | 5, 6 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
8 | | pwsdiagmhm.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) |
9 | 8 | fdiagfn 7787 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
10 | 7, 9 | mpan 702 |
. . . . 5
⊢ (𝐼 ∈ 𝑊 → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
11 | 10 | adantl 481 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
12 | 2, 5 | pwsbas 15970 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑𝑚 𝐼) = (Base‘𝑌)) |
13 | 12 | feq3d 5945 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼) ↔ 𝐹:𝐵⟶(Base‘𝑌))) |
14 | 11, 13 | mpbid 221 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(Base‘𝑌)) |
15 | | simplr 788 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
16 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
17 | 5, 16 | mndcl 17124 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
18 | 17 | 3expb 1258 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
19 | 18 | adantlr 747 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
20 | 8 | fvdiagfn 7788 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
21 | 15, 19, 20 | syl2anc 691 |
. . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
22 | 8 | fvdiagfn 7788 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = (𝐼 × {𝑎})) |
23 | 8 | fvdiagfn 7788 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = (𝐼 × {𝑏})) |
24 | 22, 23 | oveqan12d 6568 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) ∧ (𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
25 | 24 | anandis 869 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
26 | 25 | adantll 746 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
27 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) |
28 | | simpll 786 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Mnd) |
29 | 2, 5, 27 | pwsdiagel 15980 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑎 ∈ 𝐵) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) |
30 | 29 | adantrr 749 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) |
31 | 2, 5, 27 | pwsdiagel 15980 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑏 ∈ 𝐵) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) |
32 | 31 | adantrl 748 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) |
33 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
34 | 2, 27, 28, 15, 30, 32, 16, 33 | pwsplusgval 15973 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏})) = ((𝐼 × {𝑎}) ∘𝑓
(+g‘𝑅)(𝐼 × {𝑏}))) |
35 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ 𝑊) |
36 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑎 ∈ V) |
38 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑏 ∈ V) |
40 | 35, 37, 39 | ofc12 6820 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑊 → ((𝐼 × {𝑎}) ∘𝑓
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
41 | 40 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎}) ∘𝑓
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
42 | 26, 34, 41 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
43 | 21, 42 | eqtr4d 2647 |
. . . 4
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) |
44 | 43 | ralrimivva 2954 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) |
45 | | simpr 476 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
46 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
47 | 5, 46 | mndidcl 17131 |
. . . . . 6
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ 𝐵) |
48 | 47 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (0g‘𝑅) ∈ 𝐵) |
49 | 8 | fvdiagfn 7788 |
. . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ (0g‘𝑅) ∈ 𝐵) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) |
50 | 45, 48, 49 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) |
51 | 2, 46 | pws0g 17149 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐼 × {(0g‘𝑅)}) = (0g‘𝑌)) |
52 | 50, 51 | eqtrd 2644 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (0g‘𝑌)) |
53 | 14, 44, 52 | 3jca 1235 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌))) |
54 | | eqid 2610 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
55 | 5, 27, 16, 33, 46, 54 | ismhm 17160 |
. 2
⊢ (𝐹 ∈ (𝑅 MndHom 𝑌) ↔ ((𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌)))) |
56 | 4, 53, 55 | sylanbrc 695 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) |