Step | Hyp | Ref
| Expression |
1 | | prdsrngd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdsrngd.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | prdsrngd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
4 | | prdsrngd.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶Rng) |
5 | | rngabl 20045 |
. . . . 5
⊢ (𝑥 ∈ Rng → 𝑥 ∈ Abel) |
6 | 5 | ssriv 3978 |
. . . 4
⊢ Rng
⊆ Abel |
7 | | fss 6724 |
. . . 4
⊢ ((𝑅:𝐼⟶Rng ∧ Rng ⊆ Abel) →
𝑅:𝐼⟶Abel) |
8 | 4, 6, 7 | sylancl 585 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Abel) |
9 | 1, 2, 3, 8 | prdsabld 19767 |
. 2
⊢ (𝜑 → 𝑌 ∈ Abel) |
10 | | eqid 2724 |
. . . 4
⊢ (𝑆Xs(mulGrp ∘ 𝑅)) = (𝑆Xs(mulGrp ∘ 𝑅)) |
11 | | rngmgpf 20047 |
. . . . 5
⊢ (mulGrp
↾ Rng):Rng⟶Smgrp |
12 | | fco2 6734 |
. . . . 5
⊢ (((mulGrp
↾ Rng):Rng⟶Smgrp ∧ 𝑅:𝐼⟶Rng) → (mulGrp ∘ 𝑅):𝐼⟶Smgrp) |
13 | 11, 4, 12 | sylancr 586 |
. . . 4
⊢ (𝜑 → (mulGrp ∘ 𝑅):𝐼⟶Smgrp) |
14 | 10, 2, 3, 13 | prdssgrpd 18653 |
. . 3
⊢ (𝜑 → (𝑆Xs(mulGrp ∘ 𝑅)) ∈ Smgrp) |
15 | | fvexd 6896 |
. . . 4
⊢ (𝜑 → (mulGrp‘𝑌) ∈ V) |
16 | | ovexd 7436 |
. . . 4
⊢ (𝜑 → (𝑆Xs(mulGrp ∘ 𝑅)) ∈ V) |
17 | | eqidd 2725 |
. . . 4
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))) |
18 | | eqid 2724 |
. . . . . 6
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
19 | 4 | ffnd 6708 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) |
20 | 1, 18, 10, 2, 3, 19 | prdsmgp 20041 |
. . . . 5
⊢ (𝜑 →
((Base‘(mulGrp‘𝑌)) = (Base‘(𝑆Xs(mulGrp ∘ 𝑅))) ∧
(+g‘(mulGrp‘𝑌)) = (+g‘(𝑆Xs(mulGrp ∘ 𝑅))))) |
21 | 20 | simpld 494 |
. . . 4
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(𝑆Xs(mulGrp ∘ 𝑅)))) |
22 | 20 | simprd 495 |
. . . . 5
⊢ (𝜑 →
(+g‘(mulGrp‘𝑌)) = (+g‘(𝑆Xs(mulGrp ∘ 𝑅)))) |
23 | 22 | oveqdr 7429 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘(𝑆Xs(mulGrp ∘ 𝑅)))𝑦)) |
24 | 15, 16, 17, 21, 23 | sgrppropd 18651 |
. . 3
⊢ (𝜑 → ((mulGrp‘𝑌) ∈ Smgrp ↔ (𝑆Xs(mulGrp ∘ 𝑅)) ∈ Smgrp)) |
25 | 14, 24 | mpbird 257 |
. 2
⊢ (𝜑 → (mulGrp‘𝑌) ∈ Smgrp) |
26 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Rng) |
27 | 26 | ffvelcdmda 7076 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑅‘𝑤) ∈ Rng) |
28 | | eqid 2724 |
. . . . . . . . 9
⊢
(Base‘𝑌) =
(Base‘𝑌) |
29 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑆 ∈ 𝑉) |
30 | 29 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
31 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝐼 ∈ 𝑊) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
33 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑅 Fn 𝐼) |
35 | | simplr1 1212 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑥 ∈ (Base‘𝑌)) |
36 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑤 ∈ 𝐼) |
37 | 1, 28, 30, 32, 34, 35, 36 | prdsbasprj 17414 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤))) |
38 | | simpr2 1192 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑦 ∈ (Base‘𝑌)) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑦 ∈ (Base‘𝑌)) |
40 | 1, 28, 30, 32, 34, 39, 36 | prdsbasprj 17414 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤))) |
41 | | simpr3 1193 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑧 ∈ (Base‘𝑌)) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑧 ∈ (Base‘𝑌)) |
43 | 1, 28, 30, 32, 34, 42, 36 | prdsbasprj 17414 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤))) |
44 | | eqid 2724 |
. . . . . . . . 9
⊢
(Base‘(𝑅‘𝑤)) = (Base‘(𝑅‘𝑤)) |
45 | | eqid 2724 |
. . . . . . . . 9
⊢
(+g‘(𝑅‘𝑤)) = (+g‘(𝑅‘𝑤)) |
46 | | eqid 2724 |
. . . . . . . . 9
⊢
(.r‘(𝑅‘𝑤)) = (.r‘(𝑅‘𝑤)) |
47 | 44, 45, 46 | rngdi 20050 |
. . . . . . . 8
⊢ (((𝑅‘𝑤) ∈ Rng ∧ ((𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤)))) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
48 | 27, 37, 40, 43, 47 | syl13anc 1369 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
49 | | eqid 2724 |
. . . . . . . . 9
⊢
(+g‘𝑌) = (+g‘𝑌) |
50 | 1, 28, 30, 32, 34, 39, 42, 49, 36 | prdsplusgfval 17416 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑦(+g‘𝑌)𝑧)‘𝑤) = ((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) |
51 | 50 | oveq2d 7417 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
52 | | eqid 2724 |
. . . . . . . . 9
⊢
(.r‘𝑌) = (.r‘𝑌) |
53 | 1, 28, 30, 32, 34, 35, 39, 52, 36 | prdsmulrfval 17418 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(.r‘𝑌)𝑦)‘𝑤) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))) |
54 | 1, 28, 30, 32, 34, 35, 42, 52, 36 | prdsmulrfval 17418 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(.r‘𝑌)𝑧)‘𝑤) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) |
55 | 53, 54 | oveq12d 7419 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
56 | 48, 51, 55 | 3eqtr4d 2774 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)) = (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤))) |
57 | 56 | mpteq2dva 5238 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑤 ∈ 𝐼 ↦ ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤))) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)))) |
58 | | simpr1 1191 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑥 ∈ (Base‘𝑌)) |
59 | | rnggrp 20048 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Rng → 𝑥 ∈ Grp) |
60 | 59 | grpmndd 18863 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Rng → 𝑥 ∈ Mnd) |
61 | 60 | ssriv 3978 |
. . . . . . . . 9
⊢ Rng
⊆ Mnd |
62 | | fss 6724 |
. . . . . . . . 9
⊢ ((𝑅:𝐼⟶Rng ∧ Rng ⊆ Mnd) →
𝑅:𝐼⟶Mnd) |
63 | 4, 61, 62 | sylancl 585 |
. . . . . . . 8
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
64 | 63 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd) |
65 | 1, 28, 49, 29, 31, 64, 38, 41 | prdsplusgcl 18685 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑦(+g‘𝑌)𝑧) ∈ (Base‘𝑌)) |
66 | 1, 28, 29, 31, 33, 58, 65, 52 | prdsmulrval 17417 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)))) |
67 | 1, 28, 52, 29, 31, 26, 58, 38 | prdsmulrngcl 20065 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)𝑦) ∈ (Base‘𝑌)) |
68 | 1, 28, 52, 29, 31, 26, 58, 41 | prdsmulrngcl 20065 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)𝑧) ∈ (Base‘𝑌)) |
69 | 1, 28, 29, 31, 33, 67, 68, 49 | prdsplusgval 17415 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)))) |
70 | 57, 66, 69 | 3eqtr4d 2774 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧))) |
71 | 44, 45, 46 | rngdir 20051 |
. . . . . . . 8
⊢ (((𝑅‘𝑤) ∈ Rng ∧ ((𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤)))) → (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
72 | 27, 37, 40, 43, 71 | syl13anc 1369 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
73 | 1, 28, 30, 32, 34, 35, 39, 49, 36 | prdsplusgfval 17416 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(+g‘𝑌)𝑦)‘𝑤) = ((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))) |
74 | 73 | oveq1d 7416 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) |
75 | 1, 28, 30, 32, 34, 39, 42, 52, 36 | prdsmulrfval 17418 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑦(.r‘𝑌)𝑧)‘𝑤) = ((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) |
76 | 54, 75 | oveq12d 7419 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
77 | 72, 74, 76 | 3eqtr4d 2774 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤))) |
78 | 77 | mpteq2dva 5238 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑤 ∈ 𝐼 ↦ (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)))) |
79 | 1, 28, 49, 29, 31, 64, 58, 38 | prdsplusgcl 18685 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(+g‘𝑌)𝑦) ∈ (Base‘𝑌)) |
80 | 1, 28, 29, 31, 33, 79, 41, 52 | prdsmulrval 17417 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = (𝑤 ∈ 𝐼 ↦ (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
81 | 1, 28, 52, 29, 31, 26, 38, 41 | prdsmulrngcl 20065 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑦(.r‘𝑌)𝑧) ∈ (Base‘𝑌)) |
82 | 1, 28, 29, 31, 33, 68, 81, 49 | prdsplusgval 17415 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)))) |
83 | 78, 80, 82 | 3eqtr4d 2774 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧))) |
84 | 70, 83 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)))) |
85 | 84 | ralrimivvva 3195 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)∀𝑧 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)))) |
86 | 28, 18, 49, 52 | isrng 20044 |
. 2
⊢ (𝑌 ∈ Rng ↔ (𝑌 ∈ Abel ∧
(mulGrp‘𝑌) ∈
Smgrp ∧ ∀𝑥
∈ (Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)∀𝑧 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧))))) |
87 | 9, 25, 85, 86 | syl3anbrc 1340 |
1
⊢ (𝜑 → 𝑌 ∈ Rng) |