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