Step | Hyp | Ref
| Expression |
1 | | simpl 476 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ Mnd) |
2 | | pwsdiagmhm.y |
. . . 4
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
3 | 2 | pwsmnd 17678 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ Mnd) |
4 | 1, 3 | jca 507 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd)) |
5 | | pwsdiagmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
6 | 5 | fvexi 6447 |
. . . . . 6
⊢ 𝐵 ∈ V |
7 | | pwsdiagmhm.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) |
8 | 7 | fdiagfn 8168 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
9 | 6, 8 | mpan 681 |
. . . . 5
⊢ (𝐼 ∈ 𝑊 → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
10 | 9 | adantl 475 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
11 | 2, 5 | pwsbas 16500 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑𝑚 𝐼) = (Base‘𝑌)) |
12 | 11 | feq3d 6265 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼) ↔ 𝐹:𝐵⟶(Base‘𝑌))) |
13 | 10, 12 | mpbid 224 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(Base‘𝑌)) |
14 | | simplr 785 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
15 | | eqid 2825 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
16 | 5, 15 | mndcl 17654 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
17 | 16 | 3expb 1153 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
18 | 17 | adantlr 706 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
19 | 7 | fvdiagfn 8169 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
20 | 14, 18, 19 | syl2anc 579 |
. . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
21 | 7 | fvdiagfn 8169 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = (𝐼 × {𝑎})) |
22 | 7 | fvdiagfn 8169 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = (𝐼 × {𝑏})) |
23 | 21, 22 | oveqan12d 6924 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑎 ∈ 𝐵) ∧ (𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
24 | 23 | anandis 668 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
25 | 24 | adantll 705 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏}))) |
26 | | eqid 2825 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) |
27 | | simpll 783 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Mnd) |
28 | 2, 5, 26 | pwsdiagel 16510 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑎 ∈ 𝐵) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) |
29 | 28 | adantrr 708 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑎}) ∈ (Base‘𝑌)) |
30 | 2, 5, 26 | pwsdiagel 16510 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ 𝑏 ∈ 𝐵) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) |
31 | 30 | adantrl 707 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐼 × {𝑏}) ∈ (Base‘𝑌)) |
32 | | eqid 2825 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
33 | 2, 26, 27, 14, 29, 31, 15, 32 | pwsplusgval 16503 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎})(+g‘𝑌)(𝐼 × {𝑏})) = ((𝐼 × {𝑎}) ∘𝑓
(+g‘𝑅)(𝐼 × {𝑏}))) |
34 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ 𝑊) |
35 | | vex 3417 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑎 ∈ V) |
37 | | vex 3417 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → 𝑏 ∈ V) |
39 | 34, 36, 38 | ofc12 7182 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑊 → ((𝐼 × {𝑎}) ∘𝑓
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
40 | 39 | ad2antlr 718 |
. . . . . 6
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐼 × {𝑎}) ∘𝑓
(+g‘𝑅)(𝐼 × {𝑏})) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
41 | 25, 33, 40 | 3eqtrd 2865 |
. . . . 5
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) = (𝐼 × {(𝑎(+g‘𝑅)𝑏)})) |
42 | 20, 41 | eqtr4d 2864 |
. . . 4
⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) |
43 | 42 | ralrimivva 3180 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏))) |
44 | | simpr 479 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
45 | | eqid 2825 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
46 | 5, 45 | mndidcl 17661 |
. . . . . 6
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ 𝐵) |
47 | 46 | adantr 474 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (0g‘𝑅) ∈ 𝐵) |
48 | 7 | fvdiagfn 8169 |
. . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ (0g‘𝑅) ∈ 𝐵) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) |
49 | 44, 47, 48 | syl2anc 579 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (𝐼 × {(0g‘𝑅)})) |
50 | 2, 45 | pws0g 17679 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐼 × {(0g‘𝑅)}) = (0g‘𝑌)) |
51 | 49, 50 | eqtrd 2861 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹‘(0g‘𝑅)) = (0g‘𝑌)) |
52 | 13, 43, 51 | 3jca 1162 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌))) |
53 | | eqid 2825 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
54 | 5, 26, 15, 32, 45, 53 | ismhm 17690 |
. 2
⊢ (𝐹 ∈ (𝑅 MndHom 𝑌) ↔ ((𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ (𝐹:𝐵⟶(Base‘𝑌) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑌)(𝐹‘𝑏)) ∧ (𝐹‘(0g‘𝑅)) = (0g‘𝑌)))) |
55 | 4, 52, 54 | sylanbrc 578 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) |