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 17676 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Mnd) |
6 | | prdspjmhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐼) |
7 | 4, 6 | ffvelrnd 6609 |
. . 3
⊢ (𝜑 → (𝑅‘𝐴) ∈ Mnd) |
8 | 5, 7 | jca 507 |
. 2
⊢ (𝜑 → (𝑌 ∈ Mnd ∧ (𝑅‘𝐴) ∈ Mnd)) |
9 | | prdspjmhm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
10 | 3 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑆 ∈ 𝑋) |
11 | 2 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
12 | 4 | ffnd 6279 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) |
13 | 12 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 Fn 𝐼) |
14 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
15 | 6 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐼) |
16 | 1, 9, 10, 11, 13, 14, 15 | prdsbasprj 16485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥‘𝐴) ∈ (Base‘(𝑅‘𝐴))) |
17 | 16 | fmpttd 6634 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘(𝑅‘𝐴))) |
18 | 3 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑆 ∈ 𝑋) |
19 | 2 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐼 ∈ 𝑉) |
20 | 12 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑅 Fn 𝐼) |
21 | | simprl 787 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
22 | | simprr 789 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵) |
23 | | eqid 2825 |
. . . . . 6
⊢
(+g‘𝑌) = (+g‘𝑌) |
24 | 6 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐴 ∈ 𝐼) |
25 | 1, 9, 18, 19, 20, 21, 22, 23, 24 | prdsplusgfval 16487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝑌)𝑧)‘𝐴) = ((𝑦‘𝐴)(+g‘(𝑅‘𝐴))(𝑧‘𝐴))) |
26 | 9, 23 | mndcl 17654 |
. . . . . . . 8
⊢ ((𝑌 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝑌)𝑧) ∈ 𝐵) |
27 | 26 | 3expb 1153 |
. . . . . . 7
⊢ ((𝑌 ∈ Mnd ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝑌)𝑧) ∈ 𝐵) |
28 | 5, 27 | sylan 575 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝑌)𝑧) ∈ 𝐵) |
29 | | fveq1 6432 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝑌)𝑧) → (𝑥‘𝐴) = ((𝑦(+g‘𝑌)𝑧)‘𝐴)) |
30 | | eqid 2825 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) = (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) |
31 | | fvex 6446 |
. . . . . . 7
⊢ ((𝑦(+g‘𝑌)𝑧)‘𝐴) ∈ V |
32 | 29, 30, 31 | fvmpt 6529 |
. . . . . 6
⊢ ((𝑦(+g‘𝑌)𝑧) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = ((𝑦(+g‘𝑌)𝑧)‘𝐴)) |
33 | 28, 32 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = ((𝑦(+g‘𝑌)𝑧)‘𝐴)) |
34 | | fveq1 6432 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥‘𝐴) = (𝑦‘𝐴)) |
35 | | fvex 6446 |
. . . . . . . 8
⊢ (𝑦‘𝐴) ∈ V |
36 | 34, 30, 35 | fvmpt 6529 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦) = (𝑦‘𝐴)) |
37 | | fveq1 6432 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥‘𝐴) = (𝑧‘𝐴)) |
38 | | fvex 6446 |
. . . . . . . 8
⊢ (𝑧‘𝐴) ∈ V |
39 | 37, 30, 38 | fvmpt 6529 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧) = (𝑧‘𝐴)) |
40 | 36, 39 | oveqan12d 6924 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) = ((𝑦‘𝐴)(+g‘(𝑅‘𝐴))(𝑧‘𝐴))) |
41 | 40 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) = ((𝑦‘𝐴)(+g‘(𝑅‘𝐴))(𝑧‘𝐴))) |
42 | 25, 33, 41 | 3eqtr4d 2871 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧))) |
43 | 42 | ralrimivva 3180 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧))) |
44 | | eqid 2825 |
. . . . . 6
⊢
(0g‘𝑌) = (0g‘𝑌) |
45 | 9, 44 | mndidcl 17661 |
. . . . 5
⊢ (𝑌 ∈ Mnd →
(0g‘𝑌)
∈ 𝐵) |
46 | | fveq1 6432 |
. . . . . 6
⊢ (𝑥 = (0g‘𝑌) → (𝑥‘𝐴) = ((0g‘𝑌)‘𝐴)) |
47 | | fvex 6446 |
. . . . . 6
⊢
((0g‘𝑌)‘𝐴) ∈ V |
48 | 46, 30, 47 | fvmpt 6529 |
. . . . 5
⊢
((0g‘𝑌) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = ((0g‘𝑌)‘𝐴)) |
49 | 5, 45, 48 | 3syl 18 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = ((0g‘𝑌)‘𝐴)) |
50 | 1, 2, 3, 4 | prds0g 17677 |
. . . . 5
⊢ (𝜑 → (0g ∘
𝑅) =
(0g‘𝑌)) |
51 | 50 | fveq1d 6435 |
. . . 4
⊢ (𝜑 → ((0g ∘
𝑅)‘𝐴) = ((0g‘𝑌)‘𝐴)) |
52 | | fvco3 6522 |
. . . . 5
⊢ ((𝑅:𝐼⟶Mnd ∧ 𝐴 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝐴) = (0g‘(𝑅‘𝐴))) |
53 | 4, 6, 52 | syl2anc 579 |
. . . 4
⊢ (𝜑 → ((0g ∘
𝑅)‘𝐴) = (0g‘(𝑅‘𝐴))) |
54 | 49, 51, 53 | 3eqtr2d 2867 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = (0g‘(𝑅‘𝐴))) |
55 | 17, 43, 54 | 3jca 1162 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘(𝑅‘𝐴)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = (0g‘(𝑅‘𝐴)))) |
56 | | eqid 2825 |
. . 3
⊢
(Base‘(𝑅‘𝐴)) = (Base‘(𝑅‘𝐴)) |
57 | | eqid 2825 |
. . 3
⊢
(+g‘(𝑅‘𝐴)) = (+g‘(𝑅‘𝐴)) |
58 | | eqid 2825 |
. . 3
⊢
(0g‘(𝑅‘𝐴)) = (0g‘(𝑅‘𝐴)) |
59 | 9, 56, 23, 57, 44, 58 | ismhm 17690 |
. 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴)) ↔ ((𝑌 ∈ Mnd ∧ (𝑅‘𝐴) ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)):𝐵⟶(Base‘(𝑅‘𝐴)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(𝑦(+g‘𝑌)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑦)(+g‘(𝑅‘𝐴))((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴))‘(0g‘𝑌)) = (0g‘(𝑅‘𝐴))))) |
60 | 8, 55, 59 | sylanbrc 578 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴))) |