This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- Y = ( S Xs_ R )
prdsrngd.i 
|- ( ph -> I e. W )
prdsrngd.s 
|- ( ph -> S e. V )
prdsrngd.r 
|- ( ph -> R : I --> Rng )
Assertion prdsrngd 
|- ( ph -> Y e. Rng )

Proof

Step Hyp Ref Expression
1 prdsrngd.y 
 |-  Y = ( S Xs_ R )
2 prdsrngd.i 
 |-  ( ph -> I e. W )
3 prdsrngd.s 
 |-  ( ph -> S e. V )
4 prdsrngd.r 
 |-  ( ph -> R : I --> Rng )
5 rngabl 
 |-  ( x e. Rng -> x e. Abel )
6 5 ssriv 
 |-  Rng C_ Abel
7 fss 
 |-  ( ( R : I --> Rng /\ Rng C_ Abel ) -> R : I --> Abel )
8 4 6 7 sylancl 
 |-  ( ph -> R : I --> Abel )
9 1 2 3 8 prdsabld 
 |-  ( ph -> Y e. Abel )
10 eqid 
 |-  ( S Xs_ ( mulGrp o. R ) ) = ( S Xs_ ( mulGrp o. R ) )
11 rngmgpf 
 |-  ( mulGrp |` Rng ) : Rng --> Smgrp
12 fco2 
 |-  ( ( ( mulGrp |` Rng ) : Rng --> Smgrp /\ R : I --> Rng ) -> ( mulGrp o. R ) : I --> Smgrp )
13 11 4 12 sylancr 
 |-  ( ph -> ( mulGrp o. R ) : I --> Smgrp )
14 10 2 3 13 prdssgrpd 
 |-  ( ph -> ( S Xs_ ( mulGrp o. R ) ) e. Smgrp )
15 fvexd 
 |-  ( ph -> ( mulGrp ` Y ) e. _V )
16 ovexd 
 |-  ( ph -> ( S Xs_ ( mulGrp o. R ) ) e. _V )
17 eqidd 
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) )
18 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
19 4 ffnd 
 |-  ( ph -> R Fn I )
20 1 18 10 2 3 19 prdsmgp 
 |-  ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) ) )
21 20 simpld 
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) )
22 20 simprd 
 |-  ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) )
23 22 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Y ) ) /\ y e. ( Base ` ( mulGrp ` Y ) ) ) ) -> ( x ( +g ` ( mulGrp ` Y ) ) y ) = ( x ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) y ) )
24 15 16 17 21 23 sgrppropd 
 |-  ( ph -> ( ( mulGrp ` Y ) e. Smgrp <-> ( S Xs_ ( mulGrp o. R ) ) e. Smgrp ) )
25 14 24 mpbird 
 |-  ( ph -> ( mulGrp ` Y ) e. Smgrp )
26 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> R : I --> Rng )
27 26 ffvelcdmda 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( R ` w ) e. Rng )
28 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
29 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> S e. V )
30 29 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> S e. V )
31 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> I e. W )
32 31 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> I e. W )
33 19 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> R Fn I )
34 33 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> R Fn I )
35 simplr1 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> x e. ( Base ` Y ) )
36 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> w e. I )
37 1 28 30 32 34 35 36 prdsbasprj 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( x ` w ) e. ( Base ` ( R ` w ) ) )
38 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> y e. ( Base ` Y ) )
39 38 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> y e. ( Base ` Y ) )
40 1 28 30 32 34 39 36 prdsbasprj 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( y ` w ) e. ( Base ` ( R ` w ) ) )
41 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> z e. ( Base ` Y ) )
42 41 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> z e. ( Base ` Y ) )
43 1 28 30 32 34 42 36 prdsbasprj 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( z ` w ) e. ( Base ` ( R ` w ) ) )
44 eqid 
 |-  ( Base ` ( R ` w ) ) = ( Base ` ( R ` w ) )
45 eqid 
 |-  ( +g ` ( R ` w ) ) = ( +g ` ( R ` w ) )
46 eqid 
 |-  ( .r ` ( R ` w ) ) = ( .r ` ( R ` w ) )
47 44 45 46 rngdi 
 |-  ( ( ( R ` w ) e. Rng /\ ( ( x ` w ) e. ( Base ` ( R ` w ) ) /\ ( y ` w ) e. ( Base ` ( R ` w ) ) /\ ( z ` w ) e. ( Base ` ( R ` w ) ) ) ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) ( +g ` ( R ` w ) ) ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
48 27 37 40 43 47 syl13anc 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) ( +g ` ( R ` w ) ) ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
49 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
50 1 28 30 32 34 39 42 49 36 prdsplusgfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( y ( +g ` Y ) z ) ` w ) = ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) )
51 50 oveq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) = ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) ) )
52 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
53 1 28 30 32 34 35 39 52 36 prdsmulrfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ( .r ` Y ) y ) ` w ) = ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) )
54 1 28 30 32 34 35 42 52 36 prdsmulrfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ( .r ` Y ) z ) ` w ) = ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) )
55 53 54 oveq12d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) ( +g ` ( R ` w ) ) ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
56 48 51 55 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) = ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) )
57 56 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( w e. I |-> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) ) )
58 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> x e. ( Base ` Y ) )
59 rnggrp 
 |-  ( x e. Rng -> x e. Grp )
60 59 grpmndd 
 |-  ( x e. Rng -> x e. Mnd )
61 60 ssriv 
 |-  Rng C_ Mnd
62 fss 
 |-  ( ( R : I --> Rng /\ Rng C_ Mnd ) -> R : I --> Mnd )
63 4 61 62 sylancl 
 |-  ( ph -> R : I --> Mnd )
64 63 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> R : I --> Mnd )
65 1 28 49 29 31 64 38 41 prdsplusgcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( y ( +g ` Y ) z ) e. ( Base ` Y ) )
66 1 28 29 31 33 58 65 52 prdsmulrval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( w e. I |-> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) ) )
67 1 28 52 29 31 26 58 38 prdsmulrngcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) y ) e. ( Base ` Y ) )
68 1 28 52 29 31 26 58 41 prdsmulrngcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) z ) e. ( Base ` Y ) )
69 1 28 29 31 33 67 68 49 prdsplusgval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) ) )
70 57 66 69 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) )
71 44 45 46 rngdir 
 |-  ( ( ( R ` w ) e. Rng /\ ( ( x ` w ) e. ( Base ` ( R ` w ) ) /\ ( y ` w ) e. ( Base ` ( R ` w ) ) /\ ( z ` w ) e. ( Base ` ( R ` w ) ) ) ) -> ( ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ( +g ` ( R ` w ) ) ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
72 27 37 40 43 71 syl13anc 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ( +g ` ( R ` w ) ) ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
73 1 28 30 32 34 35 39 49 36 prdsplusgfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ( +g ` Y ) y ) ` w ) = ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) )
74 73 oveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) ( .r ` ( R ` w ) ) ( z ` w ) ) )
75 1 28 30 32 34 39 42 52 36 prdsmulrfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( y ( .r ` Y ) z ) ` w ) = ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) )
76 54 75 oveq12d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ( +g ` ( R ` w ) ) ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
77 72 74 76 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) )
78 77 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( w e. I |-> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) ) )
79 1 28 49 29 31 64 58 38 prdsplusgcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( +g ` Y ) y ) e. ( Base ` Y ) )
80 1 28 29 31 33 79 41 52 prdsmulrval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( w e. I |-> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
81 1 28 52 29 31 26 38 41 prdsmulrngcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( y ( .r ` Y ) z ) e. ( Base ` Y ) )
82 1 28 29 31 33 68 81 49 prdsplusgval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) ) )
83 78 80 82 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) )
84 70 83 jca 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) /\ ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) ) )
85 84 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` Y ) A. y e. ( Base ` Y ) A. z e. ( Base ` Y ) ( ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) /\ ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) ) )
86 28 18 49 52 isrng 
 |-  ( Y e. Rng <-> ( Y e. Abel /\ ( mulGrp ` Y ) e. Smgrp /\ A. x e. ( Base ` Y ) A. y e. ( Base ` Y ) A. z e. ( Base ` Y ) ( ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) /\ ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) ) ) )
87 9 25 85 86 syl3anbrc 
 |-  ( ph -> Y e. Rng )