Metamath Proof Explorer

Theorem prdsmulrngcl

Description: Closure of the multiplication in a structure product of non-unital rings. (Contributed by Mario Carneiro, 11-Mar-2015) Generalization of prdsmulrcl . (Revised by AV, 21-Feb-2025)

Ref Expression
Hypotheses prdsmulrngcl.y 
|- Y = ( S Xs_ R )
prdsmulrngcl.b 
|- B = ( Base ` Y )
prdsmulrngcl.t 
|- .x. = ( .r ` Y )
prdsmulrngcl.s 
|- ( ph -> S e. V )
prdsmulrngcl.i 
|- ( ph -> I e. W )
prdsmulrngcl.r 
|- ( ph -> R : I --> Rng )
prdsmulrngcl.f 
|- ( ph -> F e. B )
prdsmulrngcl.g 
|- ( ph -> G e. B )
Assertion prdsmulrngcl 
|- ( ph -> ( F .x. G ) e. B )

Proof

Step Hyp Ref Expression
1 prdsmulrngcl.y 
 |-  Y = ( S Xs_ R )
2 prdsmulrngcl.b 
 |-  B = ( Base ` Y )
3 prdsmulrngcl.t 
 |-  .x. = ( .r ` Y )
4 prdsmulrngcl.s 
 |-  ( ph -> S e. V )
5 prdsmulrngcl.i 
 |-  ( ph -> I e. W )
6 prdsmulrngcl.r 
 |-  ( ph -> R : I --> Rng )
7 prdsmulrngcl.f 
 |-  ( ph -> F e. B )
8 prdsmulrngcl.g 
 |-  ( ph -> G e. B )
9 6 ffnd 
 |-  ( ph -> R Fn I )
10 1 2 4 5 9 7 8 3 prdsmulrval 
 |-  ( ph -> ( F .x. G ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) )
11 6 ffvelcdmda 
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. Rng )
12 4 adantr 
 |-  ( ( ph /\ x e. I ) -> S e. V )
13 5 adantr 
 |-  ( ( ph /\ x e. I ) -> I e. W )
14 9 adantr 
 |-  ( ( ph /\ x e. I ) -> R Fn I )
15 7 adantr 
 |-  ( ( ph /\ x e. I ) -> F e. B )
16 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
17 1 2 12 13 14 15 16 prdsbasprj 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. ( Base ` ( R ` x ) ) )
18 8 adantr 
 |-  ( ( ph /\ x e. I ) -> G e. B )
19 1 2 12 13 14 18 16 prdsbasprj 
 |-  ( ( ph /\ x e. I ) -> ( G ` x ) e. ( Base ` ( R ` x ) ) )
20 eqid 
 |-  ( Base ` ( R ` x ) ) = ( Base ` ( R ` x ) )
21 eqid 
 |-  ( .r ` ( R ` x ) ) = ( .r ` ( R ` x ) )
22 20 21 rngcl 
 |-  ( ( ( R ` x ) e. Rng /\ ( F ` x ) e. ( Base ` ( R ` x ) ) /\ ( G ` x ) e. ( Base ` ( R ` x ) ) ) -> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) )
23 11 17 19 22 syl3anc 
 |-  ( ( ph /\ x e. I ) -> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) )
24 23 ralrimiva 
 |-  ( ph -> A. x e. I ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) )
25 1 2 4 5 9 prdsbasmpt 
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) e. B <-> A. x e. I ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) ) )
26 24 25 mpbird 
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) e. B )
27 10 26 eqeltrd 
 |-  ( ph -> ( F .x. G ) e. B )