Step | Hyp | Ref
| Expression |
1 | | pwsco1mhm.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Mnd) |
2 | | pwsco1mhm.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | pwsco1mhm.z |
. . . . 5
⊢ 𝑍 = (𝑅 ↑s 𝐵) |
4 | 3 | pwsmnd 17325 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → 𝑍 ∈ Mnd) |
5 | 1, 2, 4 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝑍 ∈ Mnd) |
6 | | pwsco1mhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
7 | | pwsco1mhm.y |
. . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
8 | 7 | pwsmnd 17325 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Mnd) |
9 | 1, 6, 8 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Mnd) |
10 | 5, 9 | jca 554 |
. 2
⊢ (𝜑 → (𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd)) |
11 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | | pwsco1mhm.c |
. . . . . . . . 9
⊢ 𝐶 = (Base‘𝑍) |
13 | 3, 11, 12 | pwselbasb 16148 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → (𝑔 ∈ 𝐶 ↔ 𝑔:𝐵⟶(Base‘𝑅))) |
14 | 1, 2, 13 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↔ 𝑔:𝐵⟶(Base‘𝑅))) |
15 | 14 | biimpa 501 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔:𝐵⟶(Base‘𝑅)) |
16 | | pwsco1mhm.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
17 | 16 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
18 | | fco 6058 |
. . . . . 6
⊢ ((𝑔:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
19 | 15, 17, 18 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
20 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
21 | 7, 11, 20 | pwselbasb 16148 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
22 | 1, 6, 21 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
23 | 22 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
24 | 19, 23 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → (𝑔 ∘ 𝐹) ∈ (Base‘𝑌)) |
25 | | eqid 2622 |
. . . 4
⊢ (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) = (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) |
26 | 24, 25 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌)) |
27 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐴 ∈ 𝑉) |
28 | | fvexd 6203 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝑥‘(𝐹‘𝑧)) ∈ V) |
29 | | fvexd 6203 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝑦‘(𝐹‘𝑧)) ∈ V) |
30 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹:𝐴⟶𝐵) |
31 | 30 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵) |
32 | 30 | feqmptd 6249 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))) |
33 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑅 ∈ Mnd) |
34 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐵 ∈ 𝑊) |
35 | | simprl 794 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
36 | 3, 11, 12, 33, 34, 35 | pwselbas 16149 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥:𝐵⟶(Base‘𝑅)) |
37 | 36 | feqmptd 6249 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 = (𝑤 ∈ 𝐵 ↦ (𝑥‘𝑤))) |
38 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑧) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑧))) |
39 | 31, 32, 37, 38 | fmptco 6396 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ (𝑥‘(𝐹‘𝑧)))) |
40 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
41 | 3, 11, 12, 33, 34, 40 | pwselbas 16149 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦:𝐵⟶(Base‘𝑅)) |
42 | 41 | feqmptd 6249 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 = (𝑤 ∈ 𝐵 ↦ (𝑦‘𝑤))) |
43 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑧) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑧))) |
44 | 31, 32, 42, 43 | fmptco 6396 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ (𝑦‘(𝐹‘𝑧)))) |
45 | 27, 28, 29, 39, 44 | offval2 6914 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹) ∘𝑓
(+g‘𝑅)(𝑦 ∘ 𝐹)) = (𝑧 ∈ 𝐴 ↦ ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧))))) |
46 | | fco 6058 |
. . . . . . . . 9
⊢ ((𝑥:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
47 | 36, 30, 46 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
48 | 7, 11, 20 | pwselbasb 16148 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑥 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
49 | 33, 27, 48 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
50 | 47, 49 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) ∈ (Base‘𝑌)) |
51 | | fco 6058 |
. . . . . . . . 9
⊢ ((𝑦:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
52 | 41, 30, 51 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
53 | 7, 11, 20 | pwselbasb 16148 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
54 | 33, 27, 53 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑦 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
55 | 52, 54 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) ∈ (Base‘𝑌)) |
56 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
57 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
58 | 7, 20, 33, 27, 50, 55, 56, 57 | pwsplusgval 16150 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹)) = ((𝑥 ∘ 𝐹) ∘𝑓
(+g‘𝑅)(𝑦 ∘ 𝐹))) |
59 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑍) = (+g‘𝑍) |
60 | 3, 12, 33, 34, 35, 40, 56, 59 | pwsplusgval 16150 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) = (𝑥 ∘𝑓
(+g‘𝑅)𝑦)) |
61 | | fvexd 6203 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑤 ∈ 𝐵) → (𝑥‘𝑤) ∈ V) |
62 | | fvexd 6203 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑤 ∈ 𝐵) → (𝑦‘𝑤) ∈ V) |
63 | 34, 61, 62, 37, 42 | offval2 6914 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘𝑓
(+g‘𝑅)𝑦) = (𝑤 ∈ 𝐵 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
64 | 60, 63 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) = (𝑤 ∈ 𝐵 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
65 | 38, 43 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑧) → ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)) = ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧)))) |
66 | 31, 32, 64, 65 | fmptco 6396 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧))))) |
67 | 45, 58, 66 | 3eqtr4rd 2667 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) = ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹))) |
68 | 12, 59 | mndcl 17301 |
. . . . . . . 8
⊢ ((𝑍 ∈ Mnd ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
69 | 68 | 3expb 1266 |
. . . . . . 7
⊢ ((𝑍 ∈ Mnd ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
70 | 5, 69 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
71 | | ovex 6678 |
. . . . . . 7
⊢ (𝑥(+g‘𝑍)𝑦) ∈ V |
72 | | fex 6490 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
73 | 16, 6, 72 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
74 | 73 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 ∈ V) |
75 | | coexg 7117 |
. . . . . . 7
⊢ (((𝑥(+g‘𝑍)𝑦) ∈ V ∧ 𝐹 ∈ V) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) |
76 | 71, 74, 75 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) |
77 | | coeq1 5279 |
. . . . . . 7
⊢ (𝑔 = (𝑥(+g‘𝑍)𝑦) → (𝑔 ∘ 𝐹) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
78 | 77, 25 | fvmptg 6280 |
. . . . . 6
⊢ (((𝑥(+g‘𝑍)𝑦) ∈ 𝐶 ∧ ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
79 | 70, 76, 78 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
80 | | coexg 7117 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐶 ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V) |
81 | 35, 74, 80 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) ∈ V) |
82 | | coeq1 5279 |
. . . . . . . 8
⊢ (𝑔 = 𝑥 → (𝑔 ∘ 𝐹) = (𝑥 ∘ 𝐹)) |
83 | 82, 25 | fvmptg 6280 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐶 ∧ (𝑥 ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥) = (𝑥 ∘ 𝐹)) |
84 | 35, 81, 83 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥) = (𝑥 ∘ 𝐹)) |
85 | | coexg 7117 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐶 ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V) |
86 | 40, 74, 85 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) ∈ V) |
87 | | coeq1 5279 |
. . . . . . . 8
⊢ (𝑔 = 𝑦 → (𝑔 ∘ 𝐹) = (𝑦 ∘ 𝐹)) |
88 | 87, 25 | fvmptg 6280 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐶 ∧ (𝑦 ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦) = (𝑦 ∘ 𝐹)) |
89 | 40, 86, 88 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦) = (𝑦 ∘ 𝐹)) |
90 | 84, 89 | oveq12d 6668 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) = ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹))) |
91 | 67, 79, 90 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦))) |
92 | 91 | ralrimivva 2971 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦))) |
93 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝑍) = (0g‘𝑍) |
94 | 12, 93 | mndidcl 17308 |
. . . . . 6
⊢ (𝑍 ∈ Mnd →
(0g‘𝑍)
∈ 𝐶) |
95 | 5, 94 | syl 17 |
. . . . 5
⊢ (𝜑 → (0g‘𝑍) ∈ 𝐶) |
96 | | coexg 7117 |
. . . . . 6
⊢
(((0g‘𝑍) ∈ 𝐶 ∧ 𝐹 ∈ V) →
((0g‘𝑍)
∘ 𝐹) ∈
V) |
97 | 95, 73, 96 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) ∈
V) |
98 | | coeq1 5279 |
. . . . . 6
⊢ (𝑔 = (0g‘𝑍) → (𝑔 ∘ 𝐹) = ((0g‘𝑍) ∘ 𝐹)) |
99 | 98, 25 | fvmptg 6280 |
. . . . 5
⊢
(((0g‘𝑍) ∈ 𝐶 ∧ ((0g‘𝑍) ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = ((0g‘𝑍) ∘ 𝐹)) |
100 | 95, 97, 99 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = ((0g‘𝑍) ∘ 𝐹)) |
101 | 3, 11, 12, 1, 2, 95 | pwselbas 16149 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑍):𝐵⟶(Base‘𝑅)) |
102 | | fco 6058 |
. . . . . . 7
⊢
(((0g‘𝑍):𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → ((0g‘𝑍) ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
103 | 101, 16, 102 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹):𝐴⟶(Base‘𝑅)) |
104 | | ffn 6045 |
. . . . . 6
⊢
(((0g‘𝑍) ∘ 𝐹):𝐴⟶(Base‘𝑅) → ((0g‘𝑍) ∘ 𝐹) Fn 𝐴) |
105 | 103, 104 | syl 17 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) Fn 𝐴) |
106 | | fvexd 6203 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
107 | | fnconstg 6093 |
. . . . . 6
⊢
((0g‘𝑅) ∈ V → (𝐴 × {(0g‘𝑅)}) Fn 𝐴) |
108 | 106, 107 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) Fn 𝐴) |
109 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
110 | 3, 109 | pws0g 17326 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → (𝐵 × {(0g‘𝑅)}) = (0g‘𝑍)) |
111 | 1, 2, 110 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 × {(0g‘𝑅)}) = (0g‘𝑍)) |
112 | 111 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
113 | 112 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
114 | | fvex 6201 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
115 | 16 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
116 | | fvconst2g 6467 |
. . . . . . . 8
⊢
(((0g‘𝑅) ∈ V ∧ (𝐹‘𝑥) ∈ 𝐵) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = (0g‘𝑅)) |
117 | 114, 115,
116 | sylancr 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = (0g‘𝑅)) |
118 | 113, 117 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((0g‘𝑍)‘(𝐹‘𝑥)) = (0g‘𝑅)) |
119 | | fvco3 6275 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
120 | 16, 119 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
121 | | fvconst2g 6467 |
. . . . . . 7
⊢
(((0g‘𝑅) ∈ V ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {(0g‘𝑅)})‘𝑥) = (0g‘𝑅)) |
122 | 106, 121 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {(0g‘𝑅)})‘𝑥) = (0g‘𝑅)) |
123 | 118, 120,
122 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((𝐴 × {(0g‘𝑅)})‘𝑥)) |
124 | 105, 108,
123 | eqfnfvd 6314 |
. . . 4
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) = (𝐴 ×
{(0g‘𝑅)})) |
125 | 7, 109 | pws0g 17326 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
126 | 1, 6, 125 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
127 | 100, 124,
126 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌)) |
128 | 26, 92, 127 | 3jca 1242 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌))) |
129 | | eqid 2622 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
130 | 12, 20, 59, 57, 93, 129 | ismhm 17337 |
. 2
⊢ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌) ↔ ((𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌)))) |
131 | 10, 128, 130 | sylanbrc 698 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌)) |