Step | Hyp | Ref
| Expression |
1 | | prdspjmhm.y |
. . . 4
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdspjmhm.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
3 | | prdspjmhm.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
4 | | prdspjmhm.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
5 | 1, 2, 3, 4 | prdsmndd 17146 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Mnd) |
6 | | prdspjmhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐼) |
7 | 4, 6 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝑅‘𝐴) ∈ Mnd) |
8 | 5, 7 | jca 553 |
. 2
⊢ (𝜑 → (𝑌 ∈ Mnd ∧ (𝑅‘𝐴) ∈ Mnd)) |
9 | | prdspjmhm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
10 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑆 ∈ 𝑋) |
11 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
12 | | ffn 5958 |
. . . . . . 7
⊢ (𝑅:𝐼⟶Mnd → 𝑅 Fn 𝐼) |
13 | 4, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 Fn 𝐼) |
15 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
16 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐼) |
17 | 1, 9, 10, 11, 14, 15, 16 | prdsbasprj 15955 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥‘𝐴) ∈ (Base‘(𝑅‘𝐴))) |
18 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) = (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) |
19 | 17, 18 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘(𝑅‘𝐴))) |
20 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑆 ∈ 𝑋) |
21 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐼 ∈ 𝑉) |
22 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑅 Fn 𝐼) |
23 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
24 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵) |
25 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑌) = (+g‘𝑌) |
26 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐴 ∈ 𝐼) |
27 | 1, 9, 20, 21, 22, 23, 24, 25, 26 | prdsplusgfval 15957 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝑌)𝑧)‘𝐴) = ((𝑦‘𝐴)(+g‘(𝑅‘𝐴))(𝑧‘𝐴))) |
28 | 9, 25 | mndcl 17124 |
. . . . . . . 8
⊢ ((𝑌 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝑌)𝑧) ∈ 𝐵) |
29 | 28 | 3expb 1258 |
. . . . . . 7
⊢ ((𝑌 ∈ Mnd ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝑌)𝑧) ∈ 𝐵) |
30 | 5, 29 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝑌)𝑧) ∈ 𝐵) |
31 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝑌)𝑧) → (𝑥‘𝐴) = ((𝑦(+g‘𝑌)𝑧)‘𝐴)) |
32 | | fvex 6113 |
. . . . . . 7
⊢ ((𝑦(+g‘𝑌)𝑧)‘𝐴) ∈ V |
33 | 31, 18, 32 | fvmpt 6191 |
. . . . . 6
⊢ ((𝑦(+g‘𝑌)𝑧) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = ((𝑦(+g‘𝑌)𝑧)‘𝐴)) |
34 | 30, 33 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = ((𝑦(+g‘𝑌)𝑧)‘𝐴)) |
35 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥‘𝐴) = (𝑦‘𝐴)) |
36 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑦‘𝐴) ∈ V |
37 | 35, 18, 36 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦) = (𝑦‘𝐴)) |
38 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥‘𝐴) = (𝑧‘𝐴)) |
39 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑧‘𝐴) ∈ V |
40 | 38, 18, 39 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧) = (𝑧‘𝐴)) |
41 | 37, 40 | oveqan12d 6568 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) = ((𝑦‘𝐴)(+g‘(𝑅‘𝐴))(𝑧‘𝐴))) |
42 | 41 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) = ((𝑦‘𝐴)(+g‘(𝑅‘𝐴))(𝑧‘𝐴))) |
43 | 27, 34, 42 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧))) |
44 | 43 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧))) |
45 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝑌) = (0g‘𝑌) |
46 | 9, 45 | mndidcl 17131 |
. . . . 5
⊢ (𝑌 ∈ Mnd →
(0g‘𝑌)
∈ 𝐵) |
47 | | fveq1 6102 |
. . . . . 6
⊢ (𝑥 = (0g‘𝑌) → (𝑥‘𝐴) = ((0g‘𝑌)‘𝐴)) |
48 | | fvex 6113 |
. . . . . 6
⊢
((0g‘𝑌)‘𝐴) ∈ V |
49 | 47, 18, 48 | fvmpt 6191 |
. . . . 5
⊢
((0g‘𝑌) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = ((0g‘𝑌)‘𝐴)) |
50 | 5, 46, 49 | 3syl 18 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = ((0g‘𝑌)‘𝐴)) |
51 | 1, 2, 3, 4 | prds0g 17147 |
. . . . 5
⊢ (𝜑 → (0g ∘
𝑅) =
(0g‘𝑌)) |
52 | 51 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → ((0g ∘
𝑅)‘𝐴) = ((0g‘𝑌)‘𝐴)) |
53 | | fvco3 6185 |
. . . . 5
⊢ ((𝑅:𝐼⟶Mnd ∧ 𝐴 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝐴) = (0g‘(𝑅‘𝐴))) |
54 | 4, 6, 53 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((0g ∘
𝑅)‘𝐴) = (0g‘(𝑅‘𝐴))) |
55 | 50, 52, 54 | 3eqtr2d 2650 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = (0g‘(𝑅‘𝐴))) |
56 | 19, 44, 55 | 3jca 1235 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘(𝑅‘𝐴)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = (0g‘(𝑅‘𝐴)))) |
57 | | eqid 2610 |
. . 3
⊢
(Base‘(𝑅‘𝐴)) = (Base‘(𝑅‘𝐴)) |
58 | | eqid 2610 |
. . 3
⊢
(+g‘(𝑅‘𝐴)) = (+g‘(𝑅‘𝐴)) |
59 | | eqid 2610 |
. . 3
⊢
(0g‘(𝑅‘𝐴)) = (0g‘(𝑅‘𝐴)) |
60 | 9, 57, 25, 58, 45, 59 | ismhm 17160 |
. 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴)) ↔ ((𝑌 ∈ Mnd ∧ (𝑅‘𝐴) ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘(𝑅‘𝐴)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = (0g‘(𝑅‘𝐴))))) |
61 | 8, 56, 60 | sylanbrc 695 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴))) |