Step | Hyp | Ref
| Expression |
1 | | pwsco2mhm.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
2 | | mhmrcl1 17692 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝑅 ∈ Mnd) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Mnd) |
4 | | pwsco2mhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | pwsco2mhm.y |
. . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
6 | 5 | pwsmnd 17679 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Mnd) |
7 | 3, 4, 6 | syl2anc 581 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Mnd) |
8 | | mhmrcl2 17693 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝑆 ∈ Mnd) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Mnd) |
10 | | pwsco2mhm.z |
. . . . 5
⊢ 𝑍 = (𝑆 ↑s 𝐴) |
11 | 10 | pwsmnd 17679 |
. . . 4
⊢ ((𝑆 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝑍 ∈ Mnd) |
12 | 9, 4, 11 | syl2anc 581 |
. . 3
⊢ (𝜑 → 𝑍 ∈ Mnd) |
13 | 7, 12 | jca 509 |
. 2
⊢ (𝜑 → (𝑌 ∈ Mnd ∧ 𝑍 ∈ Mnd)) |
14 | | eqid 2826 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
15 | | eqid 2826 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
16 | 14, 15 | mhmf 17694 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
17 | 1, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
18 | 17 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
19 | | pwsco2mhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
20 | 3 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑅 ∈ Mnd) |
21 | 4 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝐴 ∈ 𝑉) |
22 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ 𝐵) |
23 | 5, 14, 19, 20, 21, 22 | pwselbas 16503 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔:𝐴⟶(Base‘𝑅)) |
24 | | fco 6296 |
. . . . . 6
⊢ ((𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ 𝑔:𝐴⟶(Base‘𝑅)) → (𝐹 ∘ 𝑔):𝐴⟶(Base‘𝑆)) |
25 | 18, 23, 24 | syl2anc 581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (𝐹 ∘ 𝑔):𝐴⟶(Base‘𝑆)) |
26 | 9 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑆 ∈ Mnd) |
27 | | eqid 2826 |
. . . . . . 7
⊢
(Base‘𝑍) =
(Base‘𝑍) |
28 | 10, 15, 27 | pwselbasb 16502 |
. . . . . 6
⊢ ((𝑆 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝐹 ∘ 𝑔) ∈ (Base‘𝑍) ↔ (𝐹 ∘ 𝑔):𝐴⟶(Base‘𝑆))) |
29 | 26, 21, 28 | syl2anc 581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ((𝐹 ∘ 𝑔) ∈ (Base‘𝑍) ↔ (𝐹 ∘ 𝑔):𝐴⟶(Base‘𝑆))) |
30 | 25, 29 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (𝐹 ∘ 𝑔) ∈ (Base‘𝑍)) |
31 | 30 | fmpttd 6635 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)):𝐵⟶(Base‘𝑍)) |
32 | 1 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
33 | 32 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
34 | 32, 2 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Mnd) |
35 | 4 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐴 ∈ 𝑉) |
36 | | simprl 789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
37 | 5, 14, 19, 34, 35, 36 | pwselbas 16503 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐴⟶(Base‘𝑅)) |
38 | 37 | ffvelrnda 6609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ (Base‘𝑅)) |
39 | | simprr 791 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
40 | 5, 14, 19, 34, 35, 39 | pwselbas 16503 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐴⟶(Base‘𝑅)) |
41 | 40 | ffvelrnda 6609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝑦‘𝑤) ∈ (Base‘𝑅)) |
42 | | eqid 2826 |
. . . . . . . . . 10
⊢
(+g‘𝑅) = (+g‘𝑅) |
43 | | eqid 2826 |
. . . . . . . . . 10
⊢
(+g‘𝑆) = (+g‘𝑆) |
44 | 14, 42, 43 | mhmlin 17696 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ (𝑥‘𝑤) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑤))(+g‘𝑆)(𝐹‘(𝑦‘𝑤)))) |
45 | 33, 38, 41, 44 | syl3anc 1496 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝐹‘((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑤))(+g‘𝑆)(𝐹‘(𝑦‘𝑤)))) |
46 | 45 | mpteq2dva 4968 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑤 ∈ 𝐴 ↦ (𝐹‘((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) = (𝑤 ∈ 𝐴 ↦ ((𝐹‘(𝑥‘𝑤))(+g‘𝑆)(𝐹‘(𝑦‘𝑤))))) |
47 | | fvexd 6449 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝐹‘(𝑥‘𝑤)) ∈ V) |
48 | | fvexd 6449 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝐹‘(𝑦‘𝑤)) ∈ V) |
49 | 37 | feqmptd 6497 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 = (𝑤 ∈ 𝐴 ↦ (𝑥‘𝑤))) |
50 | 32, 16 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
51 | 50 | feqmptd 6497 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 = (𝑧 ∈ (Base‘𝑅) ↦ (𝐹‘𝑧))) |
52 | | fveq2 6434 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥‘𝑤) → (𝐹‘𝑧) = (𝐹‘(𝑥‘𝑤))) |
53 | 38, 49, 51, 52 | fmptco 6647 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ 𝑥) = (𝑤 ∈ 𝐴 ↦ (𝐹‘(𝑥‘𝑤)))) |
54 | 40 | feqmptd 6497 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 = (𝑤 ∈ 𝐴 ↦ (𝑦‘𝑤))) |
55 | | fveq2 6434 |
. . . . . . . . 9
⊢ (𝑧 = (𝑦‘𝑤) → (𝐹‘𝑧) = (𝐹‘(𝑦‘𝑤))) |
56 | 41, 54, 51, 55 | fmptco 6647 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ 𝑦) = (𝑤 ∈ 𝐴 ↦ (𝐹‘(𝑦‘𝑤)))) |
57 | 35, 47, 48, 53, 56 | offval2 7175 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹 ∘ 𝑥) ∘𝑓
(+g‘𝑆)(𝐹 ∘ 𝑦)) = (𝑤 ∈ 𝐴 ↦ ((𝐹‘(𝑥‘𝑤))(+g‘𝑆)(𝐹‘(𝑦‘𝑤))))) |
58 | 46, 57 | eqtr4d 2865 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑤 ∈ 𝐴 ↦ (𝐹‘((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) = ((𝐹 ∘ 𝑥) ∘𝑓
(+g‘𝑆)(𝐹 ∘ 𝑦))) |
59 | 34 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → 𝑅 ∈ Mnd) |
60 | 14, 42 | mndcl 17655 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (𝑥‘𝑤) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) |
61 | 59, 38, 41, 60 | syl3anc 1496 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) |
62 | | eqid 2826 |
. . . . . . . . 9
⊢
(+g‘𝑌) = (+g‘𝑌) |
63 | 5, 19, 34, 35, 36, 39, 42, 62 | pwsplusgval 16504 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑌)𝑦) = (𝑥 ∘𝑓
(+g‘𝑅)𝑦)) |
64 | | fvexd 6449 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ V) |
65 | | fvexd 6449 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐴) → (𝑦‘𝑤) ∈ V) |
66 | 35, 64, 65, 49, 54 | offval2 7175 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ∘𝑓
(+g‘𝑅)𝑦) = (𝑤 ∈ 𝐴 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
67 | 63, 66 | eqtrd 2862 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑌)𝑦) = (𝑤 ∈ 𝐴 ↦ ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
68 | | fveq2 6434 |
. . . . . . 7
⊢ (𝑧 = ((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)) → (𝐹‘𝑧) = (𝐹‘((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤)))) |
69 | 61, 67, 51, 68 | fmptco 6647 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ (𝑥(+g‘𝑌)𝑦)) = (𝑤 ∈ 𝐴 ↦ (𝐹‘((𝑥‘𝑤)(+g‘𝑅)(𝑦‘𝑤))))) |
70 | 32, 8 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ Mnd) |
71 | | fco 6296 |
. . . . . . . . 9
⊢ ((𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ 𝑥:𝐴⟶(Base‘𝑅)) → (𝐹 ∘ 𝑥):𝐴⟶(Base‘𝑆)) |
72 | 50, 37, 71 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ 𝑥):𝐴⟶(Base‘𝑆)) |
73 | 10, 15, 27 | pwselbasb 16502 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝐹 ∘ 𝑥) ∈ (Base‘𝑍) ↔ (𝐹 ∘ 𝑥):𝐴⟶(Base‘𝑆))) |
74 | 70, 35, 73 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹 ∘ 𝑥) ∈ (Base‘𝑍) ↔ (𝐹 ∘ 𝑥):𝐴⟶(Base‘𝑆))) |
75 | 72, 74 | mpbird 249 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ 𝑥) ∈ (Base‘𝑍)) |
76 | | fco 6296 |
. . . . . . . . 9
⊢ ((𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ 𝑦:𝐴⟶(Base‘𝑅)) → (𝐹 ∘ 𝑦):𝐴⟶(Base‘𝑆)) |
77 | 50, 40, 76 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ 𝑦):𝐴⟶(Base‘𝑆)) |
78 | 10, 15, 27 | pwselbasb 16502 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → ((𝐹 ∘ 𝑦) ∈ (Base‘𝑍) ↔ (𝐹 ∘ 𝑦):𝐴⟶(Base‘𝑆))) |
79 | 70, 35, 78 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹 ∘ 𝑦) ∈ (Base‘𝑍) ↔ (𝐹 ∘ 𝑦):𝐴⟶(Base‘𝑆))) |
80 | 77, 79 | mpbird 249 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ 𝑦) ∈ (Base‘𝑍)) |
81 | | eqid 2826 |
. . . . . . 7
⊢
(+g‘𝑍) = (+g‘𝑍) |
82 | 10, 27, 70, 35, 75, 80, 43, 81 | pwsplusgval 16504 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹 ∘ 𝑥)(+g‘𝑍)(𝐹 ∘ 𝑦)) = ((𝐹 ∘ 𝑥) ∘𝑓
(+g‘𝑆)(𝐹 ∘ 𝑦))) |
83 | 58, 69, 82 | 3eqtr4d 2872 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ (𝑥(+g‘𝑌)𝑦)) = ((𝐹 ∘ 𝑥)(+g‘𝑍)(𝐹 ∘ 𝑦))) |
84 | | eqid 2826 |
. . . . . 6
⊢ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) |
85 | | coeq2 5514 |
. . . . . 6
⊢ (𝑔 = (𝑥(+g‘𝑌)𝑦) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝑥(+g‘𝑌)𝑦))) |
86 | 19, 62 | mndcl 17655 |
. . . . . . . 8
⊢ ((𝑌 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑌)𝑦) ∈ 𝐵) |
87 | 86 | 3expb 1155 |
. . . . . . 7
⊢ ((𝑌 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑌)𝑦) ∈ 𝐵) |
88 | 7, 87 | sylan 577 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑌)𝑦) ∈ 𝐵) |
89 | | coexg 7380 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ (𝑥(+g‘𝑌)𝑦) ∈ 𝐵) → (𝐹 ∘ (𝑥(+g‘𝑌)𝑦)) ∈ V) |
90 | 32, 88, 89 | syl2anc 581 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹 ∘ (𝑥(+g‘𝑌)𝑦)) ∈ V) |
91 | 84, 85, 88, 90 | fvmptd3 6551 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(𝑥(+g‘𝑌)𝑦)) = (𝐹 ∘ (𝑥(+g‘𝑌)𝑦))) |
92 | | coeq2 5514 |
. . . . . . 7
⊢ (𝑔 = 𝑥 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝑥)) |
93 | 84, 92, 36, 75 | fvmptd3 6551 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑥) = (𝐹 ∘ 𝑥)) |
94 | | coeq2 5514 |
. . . . . . 7
⊢ (𝑔 = 𝑦 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝑦)) |
95 | 84, 94, 39, 80 | fvmptd3 6551 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑦) = (𝐹 ∘ 𝑦)) |
96 | 93, 95 | oveq12d 6924 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑥)(+g‘𝑍)((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑦)) = ((𝐹 ∘ 𝑥)(+g‘𝑍)(𝐹 ∘ 𝑦))) |
97 | 83, 91, 96 | 3eqtr4d 2872 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(𝑥(+g‘𝑌)𝑦)) = (((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑥)(+g‘𝑍)((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑦))) |
98 | 97 | ralrimivva 3181 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(𝑥(+g‘𝑌)𝑦)) = (((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑥)(+g‘𝑍)((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑦))) |
99 | | coeq2 5514 |
. . . . 5
⊢ (𝑔 = (0g‘𝑌) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (0g‘𝑌))) |
100 | | eqid 2826 |
. . . . . . 7
⊢
(0g‘𝑌) = (0g‘𝑌) |
101 | 19, 100 | mndidcl 17662 |
. . . . . 6
⊢ (𝑌 ∈ Mnd →
(0g‘𝑌)
∈ 𝐵) |
102 | 7, 101 | syl 17 |
. . . . 5
⊢ (𝜑 → (0g‘𝑌) ∈ 𝐵) |
103 | | coexg 7380 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ (0g‘𝑌) ∈ 𝐵) → (𝐹 ∘ (0g‘𝑌)) ∈ V) |
104 | 1, 102, 103 | syl2anc 581 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ (0g‘𝑌)) ∈ V) |
105 | 84, 99, 102, 104 | fvmptd3 6551 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(0g‘𝑌)) = (𝐹 ∘ (0g‘𝑌))) |
106 | 17 | ffnd 6280 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn (Base‘𝑅)) |
107 | | eqid 2826 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
108 | 14, 107 | mndidcl 17662 |
. . . . . . 7
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ (Base‘𝑅)) |
109 | 3, 108 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
110 | | fcoconst 6652 |
. . . . . 6
⊢ ((𝐹 Fn (Base‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝑅))
→ (𝐹 ∘ (𝐴 ×
{(0g‘𝑅)}))
= (𝐴 × {(𝐹‘(0g‘𝑅))})) |
111 | 106, 109,
110 | syl2anc 581 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ (𝐴 × {(0g‘𝑅)})) = (𝐴 × {(𝐹‘(0g‘𝑅))})) |
112 | 5, 107 | pws0g 17680 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
113 | 3, 4, 112 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝑌)) |
114 | 113 | coeq2d 5518 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ (𝐴 × {(0g‘𝑅)})) = (𝐹 ∘ (0g‘𝑌))) |
115 | | eqid 2826 |
. . . . . . . . 9
⊢
(0g‘𝑆) = (0g‘𝑆) |
116 | 107, 115 | mhm0 17697 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆)) |
117 | 1, 116 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(0g‘𝑅)) = (0g‘𝑆)) |
118 | 117 | sneqd 4410 |
. . . . . 6
⊢ (𝜑 → {(𝐹‘(0g‘𝑅))} =
{(0g‘𝑆)}) |
119 | 118 | xpeq2d 5373 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(𝐹‘(0g‘𝑅))}) = (𝐴 × {(0g‘𝑆)})) |
120 | 111, 114,
119 | 3eqtr3d 2870 |
. . . 4
⊢ (𝜑 → (𝐹 ∘ (0g‘𝑌)) = (𝐴 × {(0g‘𝑆)})) |
121 | 10, 115 | pws0g 17680 |
. . . . 5
⊢ ((𝑆 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐴 × {(0g‘𝑆)}) = (0g‘𝑍)) |
122 | 9, 4, 121 | syl2anc 581 |
. . . 4
⊢ (𝜑 → (𝐴 × {(0g‘𝑆)}) = (0g‘𝑍)) |
123 | 105, 120,
122 | 3eqtrd 2866 |
. . 3
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(0g‘𝑌)) = (0g‘𝑍)) |
124 | 31, 98, 123 | 3jca 1164 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)):𝐵⟶(Base‘𝑍) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(𝑥(+g‘𝑌)𝑦)) = (((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑥)(+g‘𝑍)((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑦)) ∧ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(0g‘𝑌)) = (0g‘𝑍))) |
125 | | eqid 2826 |
. . 3
⊢
(0g‘𝑍) = (0g‘𝑍) |
126 | 19, 27, 62, 81, 100, 125 | ismhm 17691 |
. 2
⊢ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍) ↔ ((𝑌 ∈ Mnd ∧ 𝑍 ∈ Mnd) ∧ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)):𝐵⟶(Base‘𝑍) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(𝑥(+g‘𝑌)𝑦)) = (((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑥)(+g‘𝑍)((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘𝑦)) ∧ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔))‘(0g‘𝑌)) = (0g‘𝑍)))) |
127 | 13, 124, 126 | sylanbrc 580 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍)) |