Metamath Proof Explorer

Theorem prdsrngd

Description: A product of non-unital rings is a non-unital ring. (Contributed by AV, 22-Feb-2025)

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

Proof

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