| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prdsrngd.y | . . 3
⊢ 𝑌 = (𝑆Xs𝑅) | 
| 2 |  | prdsrngd.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 3 |  | prdsrngd.s | . . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) | 
| 4 |  | prdsrngd.r | . . . 4
⊢ (𝜑 → 𝑅:𝐼⟶Rng) | 
| 5 |  | rngabl 20153 | . . . . 5
⊢ (𝑥 ∈ Rng → 𝑥 ∈ Abel) | 
| 6 | 5 | ssriv 3986 | . . . 4
⊢ Rng
⊆ Abel | 
| 7 |  | fss 6751 | . . . 4
⊢ ((𝑅:𝐼⟶Rng ∧ Rng ⊆ Abel) →
𝑅:𝐼⟶Abel) | 
| 8 | 4, 6, 7 | sylancl 586 | . . 3
⊢ (𝜑 → 𝑅:𝐼⟶Abel) | 
| 9 | 1, 2, 3, 8 | prdsabld 19881 | . 2
⊢ (𝜑 → 𝑌 ∈ Abel) | 
| 10 |  | eqid 2736 | . . . 4
⊢ (𝑆Xs(mulGrp ∘ 𝑅)) = (𝑆Xs(mulGrp ∘ 𝑅)) | 
| 11 |  | rngmgpf 20155 | . . . . 5
⊢ (mulGrp
↾ Rng):Rng⟶Smgrp | 
| 12 |  | fco2 6761 | . . . . 5
⊢ (((mulGrp
↾ Rng):Rng⟶Smgrp ∧ 𝑅:𝐼⟶Rng) → (mulGrp ∘ 𝑅):𝐼⟶Smgrp) | 
| 13 | 11, 4, 12 | sylancr 587 | . . . 4
⊢ (𝜑 → (mulGrp ∘ 𝑅):𝐼⟶Smgrp) | 
| 14 | 10, 2, 3, 13 | prdssgrpd 18747 | . . 3
⊢ (𝜑 → (𝑆Xs(mulGrp ∘ 𝑅)) ∈ Smgrp) | 
| 15 |  | fvexd 6920 | . . . 4
⊢ (𝜑 → (mulGrp‘𝑌) ∈ V) | 
| 16 |  | ovexd 7467 | . . . 4
⊢ (𝜑 → (𝑆Xs(mulGrp ∘ 𝑅)) ∈ V) | 
| 17 |  | eqidd 2737 | . . . 4
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))) | 
| 18 |  | eqid 2736 | . . . . . 6
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) | 
| 19 | 4 | ffnd 6736 | . . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) | 
| 20 | 1, 18, 10, 2, 3, 19 | prdsmgp 20149 | . . . . 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 7460 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘(𝑆Xs(mulGrp ∘ 𝑅)))𝑦)) | 
| 24 | 15, 16, 17, 21, 23 | sgrppropd 18745 | . . 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 7103 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑅‘𝑤) ∈ Rng) | 
| 28 |  | eqid 2736 | . . . . . . . . 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 1215 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑥 ∈ (Base‘𝑌)) | 
| 36 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑤 ∈ 𝐼) | 
| 37 | 1, 28, 30, 32, 34, 35, 36 | prdsbasprj 17518 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤))) | 
| 38 |  | simpr2 1195 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑦 ∈ (Base‘𝑌)) | 
| 39 | 38 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑦 ∈ (Base‘𝑌)) | 
| 40 | 1, 28, 30, 32, 34, 39, 36 | prdsbasprj 17518 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤))) | 
| 41 |  | simpr3 1196 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑧 ∈ (Base‘𝑌)) | 
| 42 | 41 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → 𝑧 ∈ (Base‘𝑌)) | 
| 43 | 1, 28, 30, 32, 34, 42, 36 | prdsbasprj 17518 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤))) | 
| 44 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘(𝑅‘𝑤)) = (Base‘(𝑅‘𝑤)) | 
| 45 |  | eqid 2736 | . . . . . . . . 9
⊢
(+g‘(𝑅‘𝑤)) = (+g‘(𝑅‘𝑤)) | 
| 46 |  | eqid 2736 | . . . . . . . . 9
⊢
(.r‘(𝑅‘𝑤)) = (.r‘(𝑅‘𝑤)) | 
| 47 | 44, 45, 46 | rngdi 20158 | . . . . . . . 8
⊢ (((𝑅‘𝑤) ∈ Rng ∧ ((𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤)))) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 48 | 27, 37, 40, 43, 47 | syl13anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 49 |  | eqid 2736 | . . . . . . . . 9
⊢
(+g‘𝑌) = (+g‘𝑌) | 
| 50 | 1, 28, 30, 32, 34, 39, 42, 49, 36 | prdsplusgfval 17520 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑦(+g‘𝑌)𝑧)‘𝑤) = ((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤))) | 
| 51 | 50 | oveq2d 7448 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦‘𝑤)(+g‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 52 |  | eqid 2736 | . . . . . . . . 9
⊢
(.r‘𝑌) = (.r‘𝑌) | 
| 53 | 1, 28, 30, 32, 34, 35, 39, 52, 36 | prdsmulrfval 17522 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(.r‘𝑌)𝑦)‘𝑤) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))) | 
| 54 | 1, 28, 30, 32, 34, 35, 42, 52, 36 | prdsmulrfval 17522 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(.r‘𝑌)𝑧)‘𝑤) = ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) | 
| 55 | 53, 54 | oveq12d 7450 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑦‘𝑤))(+g‘(𝑅‘𝑤))((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 56 | 48, 51, 55 | 3eqtr4d 2786 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)) = (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤))) | 
| 57 | 56 | mpteq2dva 5241 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑤 ∈ 𝐼 ↦ ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤))) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)))) | 
| 58 |  | simpr1 1194 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑥 ∈ (Base‘𝑌)) | 
| 59 |  | rnggrp 20156 | . . . . . . . . . . 11
⊢ (𝑥 ∈ Rng → 𝑥 ∈ Grp) | 
| 60 | 59 | grpmndd 18965 | . . . . . . . . . 10
⊢ (𝑥 ∈ Rng → 𝑥 ∈ Mnd) | 
| 61 | 60 | ssriv 3986 | . . . . . . . . 9
⊢ Rng
⊆ Mnd | 
| 62 |  | fss 6751 | . . . . . . . . 9
⊢ ((𝑅:𝐼⟶Rng ∧ Rng ⊆ Mnd) →
𝑅:𝐼⟶Mnd) | 
| 63 | 4, 61, 62 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) | 
| 64 | 63 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd) | 
| 65 | 1, 28, 49, 29, 31, 64, 38, 41 | prdsplusgcl 18782 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑦(+g‘𝑌)𝑧) ∈ (Base‘𝑌)) | 
| 66 | 1, 28, 29, 31, 33, 58, 65, 52 | prdsmulrval 17521 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ ((𝑥‘𝑤)(.r‘(𝑅‘𝑤))((𝑦(+g‘𝑌)𝑧)‘𝑤)))) | 
| 67 | 1, 28, 52, 29, 31, 26, 58, 38 | prdsmulrngcl 20173 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)𝑦) ∈ (Base‘𝑌)) | 
| 68 | 1, 28, 52, 29, 31, 26, 58, 41 | prdsmulrngcl 20173 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)𝑧) ∈ (Base‘𝑌)) | 
| 69 | 1, 28, 29, 31, 33, 67, 68, 49 | prdsplusgval 17519 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑦)‘𝑤)(+g‘(𝑅‘𝑤))((𝑥(.r‘𝑌)𝑧)‘𝑤)))) | 
| 70 | 57, 66, 69 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧))) | 
| 71 | 44, 45, 46 | rngdir 20159 | . . . . . . . 8
⊢ (((𝑅‘𝑤) ∈ Rng ∧ ((𝑥‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑦‘𝑤) ∈ (Base‘(𝑅‘𝑤)) ∧ (𝑧‘𝑤) ∈ (Base‘(𝑅‘𝑤)))) → (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 72 | 27, 37, 40, 43, 71 | syl13anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 73 | 1, 28, 30, 32, 34, 35, 39, 49, 36 | prdsplusgfval 17520 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑥(+g‘𝑌)𝑦)‘𝑤) = ((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))) | 
| 74 | 73 | oveq1d 7447 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥‘𝑤)(+g‘(𝑅‘𝑤))(𝑦‘𝑤))(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) | 
| 75 | 1, 28, 30, 32, 34, 39, 42, 52, 36 | prdsmulrfval 17522 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → ((𝑦(.r‘𝑌)𝑧)‘𝑤) = ((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) | 
| 76 | 54, 75 | oveq12d 7450 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)) = (((𝑥‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))(+g‘(𝑅‘𝑤))((𝑦‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 77 | 72, 74, 76 | 3eqtr4d 2786 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) ∧ 𝑤 ∈ 𝐼) → (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)) = (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤))) | 
| 78 | 77 | mpteq2dva 5241 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑤 ∈ 𝐼 ↦ (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤))) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)))) | 
| 79 | 1, 28, 49, 29, 31, 64, 58, 38 | prdsplusgcl 18782 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑥(+g‘𝑌)𝑦) ∈ (Base‘𝑌)) | 
| 80 | 1, 28, 29, 31, 33, 79, 41, 52 | prdsmulrval 17521 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = (𝑤 ∈ 𝐼 ↦ (((𝑥(+g‘𝑌)𝑦)‘𝑤)(.r‘(𝑅‘𝑤))(𝑧‘𝑤)))) | 
| 81 | 1, 28, 52, 29, 31, 26, 38, 41 | prdsmulrngcl 20173 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → (𝑦(.r‘𝑌)𝑧) ∈ (Base‘𝑌)) | 
| 82 | 1, 28, 29, 31, 33, 68, 81, 49 | prdsplusgval 17519 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑌) ∧ 𝑦 ∈ (Base‘𝑌) ∧ 𝑧 ∈ (Base‘𝑌))) → ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)) = (𝑤 ∈ 𝐼 ↦ (((𝑥(.r‘𝑌)𝑧)‘𝑤)(+g‘(𝑅‘𝑤))((𝑦(.r‘𝑌)𝑧)‘𝑤)))) | 
| 83 | 78, 80, 82 | 3eqtr4d 2786 | . . . 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 3204 | . 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)∀𝑧 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧)))) | 
| 86 | 28, 18, 49, 52 | isrng 20152 | . 2
⊢ (𝑌 ∈ Rng ↔ (𝑌 ∈ Abel ∧
(mulGrp‘𝑌) ∈
Smgrp ∧ ∀𝑥
∈ (Base‘𝑌)∀𝑦 ∈ (Base‘𝑌)∀𝑧 ∈ (Base‘𝑌)((𝑥(.r‘𝑌)(𝑦(+g‘𝑌)𝑧)) = ((𝑥(.r‘𝑌)𝑦)(+g‘𝑌)(𝑥(.r‘𝑌)𝑧)) ∧ ((𝑥(+g‘𝑌)𝑦)(.r‘𝑌)𝑧) = ((𝑥(.r‘𝑌)𝑧)(+g‘𝑌)(𝑦(.r‘𝑌)𝑧))))) | 
| 87 | 9, 25, 85, 86 | syl3anbrc 1343 | 1
⊢ (𝜑 → 𝑌 ∈ Rng) |