Step | Hyp | Ref
| Expression |
1 | | pwsco1mhm.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Mnd) |
2 | | pwsco1mhm.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | pwsco1mhm.z |
. . . . 5
⊢ 𝑍 = (𝑅 ↑s 𝐵) |
4 | 3 | pwsmnd 17148 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → 𝑍 ∈ Mnd) |
5 | 1, 2, 4 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑍 ∈ Mnd) |
6 | | pwsco1mhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
7 | | pwsco1mhm.y |
. . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
8 | 7 | pwsmnd 17148 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Mnd) |
9 | 1, 6, 8 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Mnd) |
10 | 5, 9 | jca 553 |
. 2
⊢ (𝜑 → (𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd)) |
11 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | | pwsco1mhm.c |
. . . . . . . . 9
⊢ 𝐶 = (Base‘𝑍) |
13 | 3, 11, 12 | pwselbasb 15971 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → (𝑔 ∈ 𝐶 ↔ 𝑔:𝐵⟶(Base‘𝑅))) |
14 | 1, 2, 13 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↔ 𝑔:𝐵⟶(Base‘𝑅))) |
15 | 14 | biimpa 500 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔:𝐵⟶(Base‘𝑅)) |
16 | | pwsco1mhm.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
18 | | fco 5971 |
. . . . . 6
⊢ ((𝑔:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
19 | 15, 17, 18 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
20 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
21 | 7, 11, 20 | pwselbasb 15971 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
22 | 1, 6, 21 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
23 | 22 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → ((𝑔 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑔 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
24 | 19, 23 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → (𝑔 ∘ 𝐹) ∈ (Base‘𝑌)) |
25 | | eqid 2610 |
. . . 4
⊢ (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) = (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) |
26 | 24, 25 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌)) |
27 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐴 ∈ 𝑉) |
28 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑥‘(𝐹‘𝑧)) ∈ V |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝑥‘(𝐹‘𝑧)) ∈ V) |
30 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑦‘(𝐹‘𝑧)) ∈ V |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝑦‘(𝐹‘𝑧)) ∈ V) |
32 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹:𝐴⟶𝐵) |
33 | 32 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵) |
34 | 32 | feqmptd 6159 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))) |
35 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑅 ∈ Mnd) |
36 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐵 ∈ 𝑊) |
37 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
38 | 3, 11, 12, 35, 36, 37 | pwselbas 15972 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥:𝐵⟶(Base‘𝑅)) |
39 | 38 | feqmptd 6159 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 = (𝑤 ∈ 𝐵 ↦ (𝑥‘𝑤))) |
40 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑧) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑧))) |
41 | 33, 34, 39, 40 | fmptco 6303 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ (𝑥‘(𝐹‘𝑧)))) |
42 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
43 | 3, 11, 12, 35, 36, 42 | pwselbas 15972 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦:𝐵⟶(Base‘𝑅)) |
44 | 43 | feqmptd 6159 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 = (𝑤 ∈ 𝐵 ↦ (𝑦‘𝑤))) |
45 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑧) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑧))) |
46 | 33, 34, 44, 45 | fmptco 6303 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ (𝑦‘(𝐹‘𝑧)))) |
47 | 27, 29, 31, 41, 46 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹) ∘𝑓
(+g‘𝑅)(𝑦 ∘ 𝐹)) = (𝑧 ∈ 𝐴 ↦ ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧))))) |
48 | | fco 5971 |
. . . . . . . . 9
⊢ ((𝑥:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
49 | 38, 32, 48 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
50 | 7, 11, 20 | pwselbasb 15971 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑥 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
51 | 35, 27, 50 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑥 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
52 | 49, 51 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) ∈ (Base‘𝑌)) |
53 | | fco 5971 |
. . . . . . . . 9
⊢ ((𝑦:𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
54 | 43, 32, 53 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
55 | 7, 11, 20 | pwselbasb 15971 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
56 | 35, 27, 55 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑦 ∘ 𝐹) ∈ (Base‘𝑌) ↔ (𝑦 ∘ 𝐹):𝐴⟶(Base‘𝑅))) |
57 | 54, 56 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) ∈ (Base‘𝑌)) |
58 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
59 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
60 | 7, 20, 35, 27, 52, 57, 58, 59 | pwsplusgval 15973 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹)) = ((𝑥 ∘ 𝐹) ∘𝑓
(+g‘𝑅)(𝑦 ∘ 𝐹))) |
61 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝑍) = (+g‘𝑍) |
62 | 3, 12, 35, 36, 37, 42, 58, 61 | pwsplusgval 15973 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) = (𝑥 ∘𝑓
(+g‘𝑅)𝑦)) |
63 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑥‘𝑤) ∈ V |
64 | 63 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑤 ∈ 𝐵) → (𝑥‘𝑤) ∈ V) |
65 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑦‘𝑤) ∈ V |
66 | 65 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ 𝑤 ∈ 𝐵) → (𝑦‘𝑤) ∈ V) |
67 | 36, 64, 66, 39, 44 | offval2 6812 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘𝑓
(+g‘𝑅)𝑦) = (𝑤 ∈ 𝐵 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
68 | 62, 67 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) = (𝑤 ∈ 𝐵 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
69 | 40, 45 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑧) → ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)) = ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧)))) |
70 | 33, 34, 68, 69 | fmptco 6303 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) = (𝑧 ∈ 𝐴 ↦ ((𝑥‘(𝐹‘𝑧))(+g‘𝑅)(𝑦‘(𝐹‘𝑧))))) |
71 | 47, 60, 70 | 3eqtr4rd 2655 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) = ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹))) |
72 | 12, 61 | mndcl 17124 |
. . . . . . . 8
⊢ ((𝑍 ∈ Mnd ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
73 | 72 | 3expb 1258 |
. . . . . . 7
⊢ ((𝑍 ∈ Mnd ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
74 | 5, 73 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝑍)𝑦) ∈ 𝐶) |
75 | | ovex 6577 |
. . . . . . 7
⊢ (𝑥(+g‘𝑍)𝑦) ∈ V |
76 | | fex 6394 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
77 | 16, 6, 76 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
78 | 77 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 ∈ V) |
79 | | coexg 7010 |
. . . . . . 7
⊢ (((𝑥(+g‘𝑍)𝑦) ∈ V ∧ 𝐹 ∈ V) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) |
80 | 75, 78, 79 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) |
81 | | coeq1 5201 |
. . . . . . 7
⊢ (𝑔 = (𝑥(+g‘𝑍)𝑦) → (𝑔 ∘ 𝐹) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
82 | 81, 25 | fvmptg 6189 |
. . . . . 6
⊢ (((𝑥(+g‘𝑍)𝑦) ∈ 𝐶 ∧ ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
83 | 74, 80, 82 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = ((𝑥(+g‘𝑍)𝑦) ∘ 𝐹)) |
84 | | coexg 7010 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐶 ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V) |
85 | 37, 78, 84 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 ∘ 𝐹) ∈ V) |
86 | | coeq1 5201 |
. . . . . . . 8
⊢ (𝑔 = 𝑥 → (𝑔 ∘ 𝐹) = (𝑥 ∘ 𝐹)) |
87 | 86, 25 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐶 ∧ (𝑥 ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥) = (𝑥 ∘ 𝐹)) |
88 | 37, 85, 87 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥) = (𝑥 ∘ 𝐹)) |
89 | | coexg 7010 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐶 ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V) |
90 | 42, 78, 89 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑦 ∘ 𝐹) ∈ V) |
91 | | coeq1 5201 |
. . . . . . . 8
⊢ (𝑔 = 𝑦 → (𝑔 ∘ 𝐹) = (𝑦 ∘ 𝐹)) |
92 | 91, 25 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐶 ∧ (𝑦 ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦) = (𝑦 ∘ 𝐹)) |
93 | 42, 90, 92 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦) = (𝑦 ∘ 𝐹)) |
94 | 88, 93 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) = ((𝑥 ∘ 𝐹)(+g‘𝑌)(𝑦 ∘ 𝐹))) |
95 | 71, 83, 94 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦))) |
96 | 95 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦))) |
97 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑍) = (0g‘𝑍) |
98 | 12, 97 | mndidcl 17131 |
. . . . . 6
⊢ (𝑍 ∈ Mnd →
(0g‘𝑍)
∈ 𝐶) |
99 | 5, 98 | syl 17 |
. . . . 5
⊢ (𝜑 → (0g‘𝑍) ∈ 𝐶) |
100 | | coexg 7010 |
. . . . . 6
⊢
(((0g‘𝑍) ∈ 𝐶 ∧ 𝐹 ∈ V) →
((0g‘𝑍)
∘ 𝐹) ∈
V) |
101 | 99, 77, 100 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) ∈
V) |
102 | | coeq1 5201 |
. . . . . 6
⊢ (𝑔 = (0g‘𝑍) → (𝑔 ∘ 𝐹) = ((0g‘𝑍) ∘ 𝐹)) |
103 | 102, 25 | fvmptg 6189 |
. . . . 5
⊢
(((0g‘𝑍) ∈ 𝐶 ∧ ((0g‘𝑍) ∘ 𝐹) ∈ V) → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = ((0g‘𝑍) ∘ 𝐹)) |
104 | 99, 101, 103 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = ((0g‘𝑍) ∘ 𝐹)) |
105 | 3, 11, 12, 1, 2, 99 | pwselbas 15972 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑍):𝐵⟶(Base‘𝑅)) |
106 | | fco 5971 |
. . . . . . 7
⊢
(((0g‘𝑍):𝐵⟶(Base‘𝑅) ∧ 𝐹:𝐴⟶𝐵) → ((0g‘𝑍) ∘ 𝐹):𝐴⟶(Base‘𝑅)) |
107 | 105, 16, 106 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹):𝐴⟶(Base‘𝑅)) |
108 | | ffn 5958 |
. . . . . 6
⊢
(((0g‘𝑍) ∘ 𝐹):𝐴⟶(Base‘𝑅) → ((0g‘𝑍) ∘ 𝐹) Fn 𝐴) |
109 | 107, 108 | syl 17 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) Fn 𝐴) |
110 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
111 | 110 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
112 | | fnconstg 6006 |
. . . . . 6
⊢
((0g‘𝑅) ∈ V → (𝐴 × {(0g‘𝑅)}) Fn 𝐴) |
113 | 111, 112 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) Fn 𝐴) |
114 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
115 | 3, 114 | pws0g 17149 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊) → (𝐵 × {(0g‘𝑅)}) = (0g‘𝑍)) |
116 | 1, 2, 115 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 × {(0g‘𝑅)}) = (0g‘𝑍)) |
117 | 116 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
118 | 117 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
119 | 16 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
120 | | fvconst2g 6372 |
. . . . . . . 8
⊢
(((0g‘𝑅) ∈ V ∧ (𝐹‘𝑥) ∈ 𝐵) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = (0g‘𝑅)) |
121 | 110, 119,
120 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 × {(0g‘𝑅)})‘(𝐹‘𝑥)) = (0g‘𝑅)) |
122 | 118, 121 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((0g‘𝑍)‘(𝐹‘𝑥)) = (0g‘𝑅)) |
123 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
124 | 16, 123 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((0g‘𝑍)‘(𝐹‘𝑥))) |
125 | | fvconst2g 6372 |
. . . . . . 7
⊢
(((0g‘𝑅) ∈ V ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {(0g‘𝑅)})‘𝑥) = (0g‘𝑅)) |
126 | 111, 125 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {(0g‘𝑅)})‘𝑥) = (0g‘𝑅)) |
127 | 122, 124,
126 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((0g‘𝑍) ∘ 𝐹)‘𝑥) = ((𝐴 × {(0g‘𝑅)})‘𝑥)) |
128 | 109, 113,
127 | eqfnfvd 6222 |
. . . 4
⊢ (𝜑 →
((0g‘𝑍)
∘ 𝐹) = (𝐴 ×
{(0g‘𝑅)})) |
129 | 7, 114 | pws0g 17149 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
130 | 1, 6, 129 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
131 | 104, 128,
130 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌)) |
132 | 26, 96, 131 | 3jca 1235 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌))) |
133 | | eqid 2610 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
134 | 12, 20, 61, 59, 97, 133 | ismhm 17160 |
. 2
⊢ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌) ↔ ((𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)):𝐶⟶(Base‘𝑌) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(𝑥(+g‘𝑍)𝑦)) = (((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑥)(+g‘𝑌)((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘𝑦)) ∧ ((𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹))‘(0g‘𝑍)) = (0g‘𝑌)))) |
135 | 10, 132, 134 | sylanbrc 695 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌)) |