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

Metamath Proof Explorer

Theorem prdsplusgsgrpcl

Description: Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025)

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

Proof

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