Metamath Proof Explorer

Theorem prdsmulrcl

Description: A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 prdsmulrcl.y 
 |-  Y = ( S Xs_ R )
2 prdsmulrcl.b 
 |-  B = ( Base ` Y )
3 prdsmulrcl.t 
 |-  .x. = ( .r ` Y )
4 prdsmulrcl.s 
 |-  ( ph -> S e. V )
5 prdsmulrcl.i 
 |-  ( ph -> I e. W )
6 prdsmulrcl.r 
 |-  ( ph -> R : I --> Ring )
7 prdsmulrcl.f 
 |-  ( ph -> F e. B )
8 prdsmulrcl.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. Ring )
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 ringcl 
 |-  ( ( ( R ` x ) e. Ring /\ ( 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 )