Step | Hyp | Ref
| Expression |
1 | | prdsringd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdsringd.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | prdsringd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
4 | | prdsringd.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶Ring) |
5 | | ringgrp 18552 |
. . . . 5
⊢ (𝑥 ∈ Ring → 𝑥 ∈ Grp) |
6 | 5 | ssriv 3607 |
. . . 4
⊢ Ring
⊆ Grp |
7 | | fss 6056 |
. . . 4
⊢ ((𝑅:𝐼⟶Ring ∧ Ring ⊆ Grp) →
𝑅:𝐼⟶Grp) |
8 | 4, 6, 7 | sylancl 694 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
9 | 1, 2, 3, 8 | prdsgrpd 17525 |
. 2
⊢ (𝜑 → 𝑌 ∈ Grp) |
10 | | eqid 2622 |
. . . 4
⊢ (𝑆Xs(mulGrp ∘ 𝑅)) = (𝑆Xs(mulGrp ∘ 𝑅)) |
11 | | mgpf 18559 |
. . . . 5
⊢ (mulGrp
↾ Ring):Ring⟶Mnd |
12 | | fco2 6059 |
. . . . 5
⊢ (((mulGrp
↾ Ring):Ring⟶Mnd ∧ 𝑅:𝐼⟶Ring) → (mulGrp ∘ 𝑅):𝐼⟶Mnd) |
13 | 11, 4, 12 | sylancr 695 |
. . . 4
⊢ (𝜑 → (mulGrp ∘ 𝑅):𝐼⟶Mnd) |
14 | 10, 2, 3, 13 | prdsmndd 17323 |
. . 3
⊢ (𝜑 → (𝑆Xs(mulGrp ∘ 𝑅)) ∈ Mnd) |
15 | | eqidd 2623 |
. . . 4
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))) |
16 | | eqid 2622 |
. . . . . 6
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
17 | | ffn 6045 |
. . . . . . 7
⊢ (𝑅:𝐼⟶Ring → 𝑅 Fn 𝐼) |
18 | 4, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) |
19 | 1, 16, 10, 2, 3, 18 | prdsmgp 18610 |
. . . . 5
⊢ (𝜑 →
((Base‘(mulGrp‘𝑌)) = (Base‘(𝑆Xs(mulGrp ∘ 𝑅))) ∧
(+g‘(mulGrp‘𝑌)) = (+g‘(𝑆Xs(mulGrp ∘ 𝑅))))) |
20 | 19 | simpld 475 |
. . . 4
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(𝑆Xs(mulGrp ∘ 𝑅)))) |
21 | 19 | simprd 479 |
. . . . 5
⊢ (𝜑 →
(+g‘(mulGrp‘𝑌)) = (+g‘(𝑆Xs(mulGrp ∘ 𝑅)))) |
22 | 21 | oveqdr 6674 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘(𝑆Xs(mulGrp ∘ 𝑅)))𝑦)) |
23 | 15, 20, 22 | mndpropd 17316 |
. . 3
⊢ (𝜑 → ((mulGrp‘𝑌) ∈ Mnd ↔ (𝑆Xs(mulGrp ∘ 𝑅)) ∈ Mnd)) |
24 | 14, 23 | mpbird 247 |
. 2
⊢ (𝜑 → (mulGrp‘𝑌) ∈ Mnd) |
25 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Ring) |
26 | 25 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑅‘𝑤) ∈ Ring) |
27 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑌) =
(Base‘𝑌) |
28 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑆 ∈ 𝑉) |
29 | 28 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
30 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝐼 ∈ 𝑊) |
31 | 30 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
32 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
33 | 32 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑅 Fn 𝐼) |
34 | | simplr1 1103 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑥 ∈ (Base‘𝑌)) |
35 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑤 ∈ 𝐼) |
36 | 1, 27, 29, 31, 33, 34, 35 | prdsbasprj 16132 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤))) |
37 | | simpr2 1068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑦 ∈ (Base‘𝑌)) |
38 | 37 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑦 ∈ (Base‘𝑌)) |
39 | 1, 27, 29, 31, 33, 38, 35 | prdsbasprj 16132 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤))) |
40 | | simpr3 1069 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑧 ∈ (Base‘𝑌)) |
41 | 40 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑧 ∈ (Base‘𝑌)) |
42 | 1, 27, 29, 31, 33, 41, 35 | prdsbasprj 16132 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤))) |
43 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘(𝑅‘𝑤)) = (Base‘(𝑅‘𝑤)) |
44 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘(𝑅‘𝑤)) = (+g‘(𝑅‘𝑤)) |
45 | | eqid 2622 |
. . . . . . . . 9
⊢
(.r‘(𝑅‘𝑤)) = (.r‘(𝑅‘𝑤)) |
46 | 43, 44, 45 | ringdi 18566 |
. . . . . . . 8
⊢ (((𝑅‘𝑤) ∈ Ring ∧ ((𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤)))) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
47 | 26, 36, 39, 42, 46 | syl13anc 1328 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
48 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑌) = (+g‘𝑌) |
49 | 1, 27, 29, 31, 33, 38, 41, 48, 35 | prdsplusgfval 16134 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑦(+g‘𝑌)𝑧)‘𝑤) = ((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) |
50 | 49 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
51 | | eqid 2622 |
. . . . . . . . 9
⊢
(.r‘𝑌) = (.r‘𝑌) |
52 | 1, 27, 29, 31, 33, 34, 38, 51, 35 | prdsmulrfval 16136 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(.r‘𝑌)𝑦)‘𝑤) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))) |
53 | 1, 27, 29, 31, 33, 34, 41, 51, 35 | prdsmulrfval 16136 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(.r‘𝑌)𝑧)‘𝑤) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) |
54 | 52, 53 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
55 | 47, 50, 54 | 3eqtr4d 2666 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)) = (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤))) |
56 | 55 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑤 ∈ 𝐼 ↦ ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤))) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)))) |
57 | | simpr1 1067 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑥 ∈ (Base‘𝑌)) |
58 | | ringmnd 18556 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Ring → 𝑥 ∈ Mnd) |
59 | 58 | ssriv 3607 |
. . . . . . . . 9
⊢ Ring
⊆ Mnd |
60 | | fss 6056 |
. . . . . . . . 9
⊢ ((𝑅:𝐼⟶Ring ∧ Ring ⊆ Mnd) →
𝑅:𝐼⟶Mnd) |
61 | 4, 59, 60 | sylancl 694 |
. . . . . . . 8
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
62 | 61 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd) |
63 | 1, 27, 48, 28, 30, 62, 37, 40 | prdsplusgcl 17321 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑦(+g‘𝑌)𝑧) ∈ (Base‘𝑌)) |
64 | 1, 27, 28, 30, 32, 57, 63, 51 | prdsmulrval 16135 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)))) |
65 | 1, 27, 51, 28, 30, 25, 57, 37 | prdsmulrcl 18611 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)𝑦) ∈ (Base‘𝑌)) |
66 | 1, 27, 51, 28, 30, 25, 57, 40 | prdsmulrcl 18611 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)𝑧) ∈ (Base‘𝑌)) |
67 | 1, 27, 28, 30, 32, 65, 66, 48 | prdsplusgval 16133 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)))) |
68 | 56, 64, 67 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧))) |
69 | 43, 44, 45 | ringdir 18567 |
. . . . . . . 8
⊢ (((𝑅‘𝑤) ∈ Ring ∧ ((𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤)))) → (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
70 | 26, 36, 39, 42, 69 | syl13anc 1328 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
71 | 1, 27, 29, 31, 33, 34, 38, 48, 35 | prdsplusgfval 16134 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(+g‘𝑌)𝑦)‘𝑤) = ((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))) |
72 | 71 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) |
73 | 1, 27, 29, 31, 33, 38, 41, 51, 35 | prdsmulrfval 16136 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑦(.r‘𝑌)𝑧)‘𝑤) = ((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) |
74 | 53, 73 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
75 | 70, 72, 74 | 3eqtr4d 2666 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤))) |
76 | 75 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑤 ∈ 𝐼 ↦ (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)))) |
77 | 1, 27, 48, 28, 30, 62, 57, 37 | prdsplusgcl 17321 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(+g‘𝑌)𝑦) ∈ (Base‘𝑌)) |
78 | 1, 27, 28, 30, 32, 77, 40, 51 | prdsmulrval 16135 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = (𝑤 ∈ 𝐼 ↦ (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) |
79 | 1, 27, 51, 28, 30, 25, 37, 40 | prdsmulrcl 18611 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑦(.r‘𝑌)𝑧) ∈ (Base‘𝑌)) |
80 | 1, 27, 28, 30, 32, 66, 79, 48 | prdsplusgval 16133 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)))) |
81 | 76, 78, 80 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧))) |
82 | 68, 81 | jca 554 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)))) |
83 | 82 | ralrimivvva 2972 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)∀𝑧 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)))) |
84 | 27, 16, 48, 51 | isring 18551 |
. 2
⊢ (𝑌 ∈ Ring ↔ (𝑌 ∈ Grp ∧
(mulGrp‘𝑌) ∈ Mnd
∧ ∀𝑥 ∈
(Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)∀𝑧 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧))))) |
85 | 9, 24, 83, 84 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝑌 ∈ Ring) |