Metamath Proof Explorer

Theorem prdsringd

Description: A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses prdsringd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsringd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsringd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsringd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Ring )
Assertion prdsringd ( 𝜑 → 𝑌 ∈ Ring )

Proof

Step Hyp Ref Expression
1 prdsringd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsringd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3 prdsringd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdsringd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Ring )
5 ringgrp ⊢ ( 𝑥 ∈ Ring → 𝑥 ∈ Grp )
6 5 ssriv ⊢ Ring ⊆ Grp
7 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ Ring ∧ Ring ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp )
8 4 6 7 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
9 1 2 3 8 prdsgrpd ⊢ ( 𝜑 → 𝑌 ∈ Grp )
10 eqid ⊢ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) = ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) )
11 mgpf ⊢ ( mulGrp ↾ Ring ) : Ring ⟶ Mnd
12 fco2 ⊢ ( ( ( mulGrp ↾ Ring ) : Ring ⟶ Mnd ∧ 𝑅 : 𝐼 ⟶ Ring ) → ( mulGrp ∘ 𝑅 ) : 𝐼 ⟶ Mnd )
13 11 4 12 sylancr ⊢ ( 𝜑 → ( mulGrp ∘ 𝑅 ) : 𝐼 ⟶ Mnd )
14 10 2 3 13 prdsmndd ⊢ ( 𝜑 → ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ∈ Mnd )
15 eqidd ⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) ) )
16 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
17 4 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
18 1 16 10 2 3 17 prdsmgp ⊢ ( 𝜑 → ( ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) ∧ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) ) )
19 18 simpld ⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
20 18 simprd ⊢ ( 𝜑 → ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
21 20 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ∧ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑌 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) 𝑦 ) )
22 15 19 21 mndpropd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑌 ) ∈ Mnd ↔ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ∈ Mnd ) )
23 14 22 mpbird ⊢ ( 𝜑 → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
24 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ Ring )
25 24 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑤 ) ∈ Ring )
26 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
27 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ 𝑉 )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
29 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ 𝑊 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
31 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 Fn 𝐼 )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
33 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝑥 ∈ ( Base ‘ 𝑌 ) )
34 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝑤 ∈ 𝐼 )
35 1 26 28 30 32 33 34 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) )
36 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑌 ) )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝑦 ∈ ( Base ‘ 𝑌 ) )
38 1 26 28 30 32 37 34 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) )
39 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑌 ) )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → 𝑧 ∈ ( Base ‘ 𝑌 ) )
41 1 26 28 30 32 40 34 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) )
42 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑤 ) )
43 eqid ⊢ ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑤 ) )
44 eqid ⊢ ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) = ( .r ‘ ( 𝑅 ‘ 𝑤 ) )
45 42 43 44 ringdi ⊢ ( ( ( 𝑅 ‘ 𝑤 ) ∈ Ring ∧ ( ( 𝑥 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) ∧ ( 𝑦 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) ∧ ( 𝑧 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) ) ) → ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
46 25 35 38 41 45 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
47 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
48 1 26 28 30 32 37 40 47 34 prdsplusgfval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) = ( ( 𝑦 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) )
49 48 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) = ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
50 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
51 1 26 28 30 32 33 37 50 34 prdsmulrfval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) = ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) )
52 1 26 28 30 32 33 40 50 34 prdsmulrfval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) = ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) )
53 51 52 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
54 46 49 53 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) = ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) )
55 54 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑤 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐼 ↦ ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) ) )
56 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑌 ) )
57 ringmnd ⊢ ( 𝑥 ∈ Ring → 𝑥 ∈ Mnd )
58 57 ssriv ⊢ Ring ⊆ Mnd
59 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ Ring ∧ Ring ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd )
60 4 58 59 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ Mnd )
62 1 26 47 27 29 61 36 39 prdsplusgcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ∈ ( Base ‘ 𝑌 ) )
63 1 26 27 29 31 56 62 50 prdsmulrval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑥 ( .r ‘ 𝑌 ) ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( 𝑤 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) ) )
64 1 26 50 27 29 24 56 36 prdsmulrcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ∈ ( Base ‘ 𝑌 ) )
65 1 26 50 27 29 24 56 39 prdsmulrcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ∈ ( Base ‘ 𝑌 ) )
66 1 26 27 29 31 64 65 47 prdsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ( +g ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ) = ( 𝑤 ∈ 𝐼 ↦ ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) ) )
67 55 63 66 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑥 ( .r ‘ 𝑌 ) ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ( +g ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ) )
68 42 43 44 ringdir ⊢ ( ( ( 𝑅 ‘ 𝑤 ) ∈ Ring ∧ ( ( 𝑥 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) ∧ ( 𝑦 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) ∧ ( 𝑧 ‘ 𝑤 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑤 ) ) ) ) → ( ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
69 25 35 38 41 68 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
70 1 26 28 30 32 33 37 47 34 prdsplusgfval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) = ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) )
71 70 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑦 ‘ 𝑤 ) ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) )
72 1 26 28 30 32 37 40 50 34 prdsmulrfval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) = ( ( 𝑦 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) )
73 52 72 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) = ( ( ( 𝑥 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
74 69 71 73 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑤 ∈ 𝐼 ) → ( ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) = ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) )
75 74 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑤 ∈ 𝐼 ↦ ( ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐼 ↦ ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) ) )
76 1 26 47 27 29 61 56 36 prdsplusgcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ∈ ( Base ‘ 𝑌 ) )
77 1 26 27 29 31 76 39 50 prdsmulrval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ( .r ‘ 𝑌 ) 𝑧 ) = ( 𝑤 ∈ 𝐼 ↦ ( ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ‘ 𝑤 ) ( .r ‘ ( 𝑅 ‘ 𝑤 ) ) ( 𝑧 ‘ 𝑤 ) ) ) )
78 1 26 50 27 29 24 36 39 prdsmulrcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ∈ ( Base ‘ 𝑌 ) )
79 1 26 27 29 31 65 78 47 prdsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ( +g ‘ 𝑌 ) ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ) = ( 𝑤 ∈ 𝐼 ↦ ( ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ( +g ‘ ( 𝑅 ‘ 𝑤 ) ) ( ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ‘ 𝑤 ) ) ) )
80 75 77 79 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ( .r ‘ 𝑌 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ( +g ‘ 𝑌 ) ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ) )
81 67 80 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑌 ) ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ( +g ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ( .r ‘ 𝑌 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ( +g ‘ 𝑌 ) ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ) ) )
82 81 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑌 ) ∀ 𝑦 ∈ ( Base ‘ 𝑌 ) ∀ 𝑧 ∈ ( Base ‘ 𝑌 ) ( ( 𝑥 ( .r ‘ 𝑌 ) ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ( +g ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ( .r ‘ 𝑌 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ( +g ‘ 𝑌 ) ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ) ) )
83 26 16 47 50 isring ⊢ ( 𝑌 ∈ Ring ↔ ( 𝑌 ∈ Grp ∧ ( mulGrp ‘ 𝑌 ) ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑌 ) ∀ 𝑦 ∈ ( Base ‘ 𝑌 ) ∀ 𝑧 ∈ ( Base ‘ 𝑌 ) ( ( 𝑥 ( .r ‘ 𝑌 ) ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) ( +g ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) ( .r ‘ 𝑌 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑌 ) 𝑧 ) ( +g ‘ 𝑌 ) ( 𝑦 ( .r ‘ 𝑌 ) 𝑧 ) ) ) ) )
84 9 23 82 83 syl3anbrc ⊢ ( 𝜑 → 𝑌 ∈ Ring )