Metamath Proof Explorer

Theorem prdsplusgcl

Description: Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 prdsplusgcl.y 
 |-  Y = ( S Xs_ R )
2 prdsplusgcl.b 
 |-  B = ( Base ` Y )
3 prdsplusgcl.p 
 |-  .+ = ( +g ` Y )
4 prdsplusgcl.s 
 |-  ( ph -> S e. V )
5 prdsplusgcl.i 
 |-  ( ph -> I e. W )
6 prdsplusgcl.r 
 |-  ( ph -> R : I --> Mnd )
7 prdsplusgcl.f 
 |-  ( ph -> F e. B )
8 prdsplusgcl.g 
 |-  ( ph -> G e. B )
9 6 ffnd 
 |-  ( ph -> R Fn I )
10 1 2 4 5 9 7 8 3 prdsplusgval 
 |-  ( ph -> ( F .+ G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )
11 6 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. Mnd )
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 
 |-  ( +g ` ( R ` x ) ) = ( +g ` ( R ` x ) )
22 20 21 mndcl 
 |-  ( ( ( R ` x ) e. Mnd /\ ( F ` x ) e. ( Base ` ( R ` x ) ) /\ ( G ` x ) e. ( Base ` ( R ` x ) ) ) -> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) )
23 11 17 19 22 syl3anc 
 |-  ( ( ph /\ x e. I ) -> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) )
24 23 ralrimiva 
 |-  ( ph -> A. x e. I ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) )
25 1 2 4 5 9 prdsbasmpt 
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) e. B <-> A. x e. I ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) ) )
26 24 25 mpbird 
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) e. B )
27 10 26 eqeltrd 
 |-  ( ph -> ( F .+ G ) e. B )