Step | Hyp | Ref
| Expression |
1 | | pwsco1mhm.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Mnd) |
2 | | pwsco1mhm.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | pwsco1mhm.z |
. . . 4
⊢ 𝑍 = (𝑅 ↑s 𝐵) |
4 | 3 | pwsmnd 18420 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → 𝑍 ∈ Mnd) |
5 | 1, 2, 4 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑍 ∈ Mnd) |
6 | | pwsco1mhm.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
7 | | pwsco1mhm.y |
. . . 4
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
8 | 7 | pwsmnd 18420 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Mnd) |
9 | 1, 6, 8 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑌 ∈ Mnd) |
10 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
11 | | pwsco1mhm.c |
. . . . . . . . 9
⊢ 𝐶 = (Base‘𝑍) |
12 | 3, 10, 11 | pwselbasb 17199 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → (𝑔 ∈ 𝐶 ↔ 𝑔:𝐵⟶(Base‘𝑅))) |
13 | 1, 2, 12 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↔ 𝑔:𝐵⟶(Base‘𝑅))) |
14 | 13 | biimpa 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔:𝐵⟶(Base‘𝑅)) |
15 | | pwsco1mhm.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
17 | | fco 6624 |
. . . . . 6
⊢ ((𝑔:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
18 | 14, 16, 17 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
19 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
20 | 7, 10, 19 | pwselbasb 17199 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
21 | 1, 6, 20 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
22 | 21 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
23 | 18, 22 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → (𝑔 ∘ 𝐹) ∈ (Base‘𝑌)) |
24 | 23 | fmpttd 6989 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌)) |
25 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐴 ∈ 𝑉) |
26 | | fvexd 6789 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝑥‘(𝐹‘𝑧)) ∈ V) |
27 | | fvexd 6789 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝑦‘(𝐹‘𝑧)) ∈ V) |
28 | 15 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹:𝐴⟶𝐵) |
29 | 28 | ffvelrnda 6961 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵) |
30 | 28 | feqmptd 6837 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))) |
31 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑅 ∈ Mnd) |
32 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐵 ∈ 𝑊) |
33 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
34 | 3, 10, 11, 31, 32, 33 | pwselbas 17200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥:𝐵⟶(Base‘𝑅)) |
35 | 34 | feqmptd 6837 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 = (𝑤 ∈ 𝐵 ↦ (𝑥‘𝑤))) |
36 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑧) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑧))) |
37 | 29, 30, 35, 36 | fmptco 7001 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ (𝑥‘(𝐹‘𝑧)))) |
38 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
39 | 3, 10, 11, 31, 32, 38 | pwselbas 17200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦:𝐵⟶(Base‘𝑅)) |
40 | 39 | feqmptd 6837 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 = (𝑤 ∈ 𝐵 ↦ (𝑦‘𝑤))) |
41 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑧) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑧))) |
42 | 29, 30, 40, 41 | fmptco 7001 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ (𝑦‘(𝐹‘𝑧)))) |
43 | 25, 26, 27, 37, 42 | offval2 7553 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹) ∘f
(+g‘𝑅)(𝑦 ∘ 𝐹)) = (𝑧 ∈ 𝐴 ↦ ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧))))) |
44 | | fco 6624 |
. . . . . . . . 9
⊢ ((𝑥:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
45 | 34, 28, 44 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
46 | 7, 10, 19 | pwselbasb 17199 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑥 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
47 | 31, 25, 46 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
48 | 45, 47 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) ∈ (Base‘𝑌)) |
49 | | fco 6624 |
. . . . . . . . 9
⊢ ((𝑦:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
50 | 39, 28, 49 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
51 | 7, 10, 19 | pwselbasb 17199 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
52 | 31, 25, 51 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑦 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
53 | 50, 52 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) ∈ (Base‘𝑌)) |
54 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
55 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
56 | 7, 19, 31, 25, 48, 53, 54, 55 | pwsplusgval 17201 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹)) = ((𝑥 ∘ 𝐹) ∘f
(+g‘𝑅)(𝑦 ∘ 𝐹))) |
57 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝑍) = (+g‘𝑍) |
58 | 3, 11, 31, 32, 33, 38, 54, 57 | pwsplusgval 17201 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) = (𝑥 ∘f
(+g‘𝑅)𝑦)) |
59 | | fvexd 6789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑤 ∈ 𝐵) → (𝑥‘𝑤) ∈ V) |
60 | | fvexd 6789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑤 ∈ 𝐵) → (𝑦‘𝑤) ∈ V) |
61 | 32, 59, 60, 35, 40 | offval2 7553 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘f
(+g‘𝑅)𝑦) = (𝑤 ∈ 𝐵 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
62 | 58, 61 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) = (𝑤 ∈ 𝐵 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
63 | 36, 41 | oveq12d 7293 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑧) → ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)) = ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧)))) |
64 | 29, 30, 62, 63 | fmptco 7001 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧))))) |
65 | 43, 56, 64 | 3eqtr4rd 2789 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) = ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹))) |
66 | | eqid 2738 |
. . . . . 6
⊢ (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) = (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) |
67 | | coeq1 5766 |
. . . . . 6
⊢ (𝑔 = (𝑥(+g‘𝑍)𝑦) → (𝑔 ∘ 𝐹) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
68 | 11, 57 | mndcl 18393 |
. . . . . . . 8
⊢ ((𝑍 ∈ Mnd ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
69 | 68 | 3expb 1119 |
. . . . . . 7
⊢ ((𝑍 ∈ Mnd ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
70 | 5, 69 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
71 | | ovex 7308 |
. . . . . . 7
⊢ (𝑥(+g‘𝑍)𝑦) ∈ V |
72 | 15, 6 | fexd 7103 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
73 | 72 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 ∈ V) |
74 | | coexg 7776 |
. . . . . . 7
⊢ (((𝑥(+g‘𝑍)𝑦) ∈ V ∧ 𝐹 ∈ V) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) |
75 | 71, 73, 74 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) |
76 | 66, 67, 70, 75 | fvmptd3 6898 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
77 | | coeq1 5766 |
. . . . . . 7
⊢ (𝑔 = 𝑥 → (𝑔 ∘ 𝐹) = (𝑥 ∘ 𝐹)) |
78 | | coexg 7776 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐶 ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V) |
79 | 33, 73, 78 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) ∈ V) |
80 | 66, 77, 33, 79 | fvmptd3 6898 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥) = (𝑥 ∘ 𝐹)) |
81 | | coeq1 5766 |
. . . . . . 7
⊢ (𝑔 = 𝑦 → (𝑔 ∘ 𝐹) = (𝑦 ∘ 𝐹)) |
82 | | coexg 7776 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐶 ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V) |
83 | 38, 73, 82 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) ∈ V) |
84 | 66, 81, 38, 83 | fvmptd3 6898 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦) = (𝑦 ∘ 𝐹)) |
85 | 80, 84 | oveq12d 7293 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) = ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹))) |
86 | 65, 76, 85 | 3eqtr4d 2788 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦))) |
87 | 86 | ralrimivva 3123 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦))) |
88 | | coeq1 5766 |
. . . . 5
⊢ (𝑔 = (0g‘𝑍) → (𝑔 ∘ 𝐹) = ((0g‘𝑍) ∘ 𝐹)) |
89 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝑍) = (0g‘𝑍) |
90 | 11, 89 | mndidcl 18400 |
. . . . . 6
⊢ (𝑍 ∈ Mnd →
(0g‘𝑍)
∈ 𝐶) |
91 | 5, 90 | syl 17 |
. . . . 5
⊢ (𝜑 → (0g‘𝑍) ∈ 𝐶) |
92 | | coexg 7776 |
. . . . . 6
⊢
(((0g‘𝑍) ∈ 𝐶 ∧ 𝐹 ∈ V) →
((0g‘𝑍)
∘ 𝐹) ∈
V) |
93 | 91, 72, 92 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) ∈
V) |
94 | 66, 88, 91, 93 | fvmptd3 6898 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = ((0g‘𝑍) ∘ 𝐹)) |
95 | 3, 10, 11, 1, 2, 91 | pwselbas 17200 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑍):𝐵⟶(Base‘𝑅)) |
96 | | fco 6624 |
. . . . . . 7
⊢
(((0g‘𝑍):𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → ((0g‘𝑍) ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
97 | 95, 15, 96 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹):𝐴⟶(Base‘𝑅)) |
98 | 97 | ffnd 6601 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) Fn 𝐴) |
99 | | fvexd 6789 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
100 | | fnconstg 6662 |
. . . . . 6
⊢
((0g‘𝑅) ∈ V → (𝐴 × {(0g‘𝑅)}) Fn 𝐴) |
101 | 99, 100 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) Fn 𝐴) |
102 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
103 | 3, 102 | pws0g 18421 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → (𝐵 × {(0g‘𝑅)}) = (0g‘𝑍)) |
104 | 1, 2, 103 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 × {(0g‘𝑅)}) = (0g‘𝑍)) |
105 | 104 | fveq1d 6776 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
106 | 105 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
107 | | fvex 6787 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
108 | 15 | ffvelrnda 6961 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
109 | | fvconst2g 7077 |
. . . . . . . 8
⊢
(((0g‘𝑅) ∈ V ∧ (𝐹‘𝑥) ∈ 𝐵) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = (0g‘𝑅)) |
110 | 107, 108,
109 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = (0g‘𝑅)) |
111 | 106, 110 | eqtr3d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((0g‘𝑍)‘(𝐹‘𝑥)) = (0g‘𝑅)) |
112 | | fvco3 6867 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
113 | 15, 112 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
114 | | fvconst2g 7077 |
. . . . . . 7
⊢
(((0g‘𝑅) ∈ V ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {(0g‘𝑅)})‘𝑥) = (0g‘𝑅)) |
115 | 99, 114 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {(0g‘𝑅)})‘𝑥) = (0g‘𝑅)) |
116 | 111, 113,
115 | 3eqtr4d 2788 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((𝐴 × {(0g‘𝑅)})‘𝑥)) |
117 | 98, 101, 116 | eqfnfvd 6912 |
. . . 4
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) = (𝐴 ×
{(0g‘𝑅)})) |
118 | 7, 102 | pws0g 18421 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
119 | 1, 6, 118 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
120 | 94, 117, 119 | 3eqtrd 2782 |
. . 3
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌)) |
121 | 24, 87, 120 | 3jca 1127 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌))) |
122 | | eqid 2738 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
123 | 11, 19, 57, 55, 89, 122 | ismhm 18432 |
. 2
⊢ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌) ↔ ((𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌)))) |
124 | 5, 9, 121, 123 | syl21anbrc 1343 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌)) |