prdssgrpd

Description: The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025)

	Ref	Expression
Hypotheses	prdssgrpd.y	$⊢ Y = S ⨉_{𝑠} R$
	prdssgrpd.i	$⊢ φ \to I \in W$
	prdssgrpd.s	$⊢ φ \to S \in V$
	prdssgrpd.r	$⊢ φ \to R : I ⟶ Smgrp$
Assertion	prdssgrpd	$⊢ φ \to Y \in Smgrp$

Proof

Step	Hyp	Ref	Expression
1		prdssgrpd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdssgrpd.i	$⊢ φ \to I \in W$
3		prdssgrpd.s	$⊢ φ \to S \in V$
4		prdssgrpd.r	$⊢ φ \to R : I ⟶ Smgrp$
5		eqidd	$⊢ φ \to {Base}_{Y} = {Base}_{Y}$
6		eqidd	$⊢ φ \to +_{Y} = +_{Y}$
7		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
8		eqid	$⊢ +_{Y} = +_{Y}$
9	3	elexd	$⊢ φ \to S \in V$
10	9	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to S \in V$
11	2	elexd	$⊢ φ \to I \in V$
12	11	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to I \in V$
13	4	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to R : I ⟶ Smgrp$
14		simprl	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to a \in {Base}_{Y}$
15		simprr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to b \in {Base}_{Y}$
16	1 7 8 10 12 13 14 15	prdsplusgsgrpcl	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to a +_{Y} b \in {Base}_{Y}$
17	16	3impb	$⊢ (φ \land a \in {Base}_{Y} \land b \in {Base}_{Y}) \to a +_{Y} b \in {Base}_{Y}$
18	4	ffvelcdmda	$⊢ (φ \land y \in I) \to R (y) \in Smgrp$
19	18	adantlr	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to R (y) \in Smgrp$
20	9	ad2antrr	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to S \in V$
21	11	ad2antrr	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to I \in V$
22	4	ffnd	$⊢ φ \to R Fn I$
23	22	ad2antrr	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to R Fn I$
24		simplr1	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a \in {Base}_{Y}$
25		simpr	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to y \in I$
26	1 7 20 21 23 24 25	prdsbasprj	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a (y) \in {Base}_{R (y)}$
27		simplr2	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to b \in {Base}_{Y}$
28	1 7 20 21 23 27 25	prdsbasprj	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to b (y) \in {Base}_{R (y)}$
29		simplr3	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to c \in {Base}_{Y}$
30	1 7 20 21 23 29 25	prdsbasprj	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to c (y) \in {Base}_{R (y)}$
31		eqid	$⊢ {Base}_{R (y)} = {Base}_{R (y)}$
32		eqid	$⊢ +_{R (y)} = +_{R (y)}$
33	31 32	sgrpass	$⊢ (R (y) \in Smgrp \land (a (y) \in {Base}_{R (y)} \land b (y) \in {Base}_{R (y)} \land c (y) \in {Base}_{R (y)})) \to (a (y) +_{R (y)} b (y)) +_{R (y)} c (y) = a (y) +_{R (y)} (b (y) +_{R (y)} c (y))$
34	19 26 28 30 33	syl13anc	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a (y) +_{R (y)} b (y)) +_{R (y)} c (y) = a (y) +_{R (y)} (b (y) +_{R (y)} c (y))$
35	1 7 20 21 23 24 27 8 25	prdsplusgfval	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a +_{Y} b) (y) = a (y) +_{R (y)} b (y)$
36	35	oveq1d	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a +_{Y} b) (y) +_{R (y)} c (y) = (a (y) +_{R (y)} b (y)) +_{R (y)} c (y)$
37	1 7 20 21 23 27 29 8 25	prdsplusgfval	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (b +_{Y} c) (y) = b (y) +_{R (y)} c (y)$
38	37	oveq2d	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a (y) +_{R (y)} (b +_{Y} c) (y) = a (y) +_{R (y)} (b (y) +_{R (y)} c (y))$
39	34 36 38	3eqtr4d	$⊢ ((φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a +_{Y} b) (y) +_{R (y)} c (y) = a (y) +_{R (y)} (b +_{Y} c) (y)$
40	39	mpteq2dva	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to (y \in I ⟼ (a +_{Y} b) (y) +_{R (y)} c (y)) = (y \in I ⟼ a (y) +_{R (y)} (b +_{Y} c) (y))$
41	9	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to S \in V$
42	11	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to I \in V$
43	22	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to R Fn I$
44	16	3adantr3	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a +_{Y} b \in {Base}_{Y}$
45		simpr3	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to c \in {Base}_{Y}$
46	1 7 41 42 43 44 45 8	prdsplusgval	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to (a +_{Y} b) +_{Y} c = (y \in I ⟼ (a +_{Y} b) (y) +_{R (y)} c (y))$
47		simpr1	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a \in {Base}_{Y}$
48	4	adantr	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to R : I ⟶ Smgrp$
49		simpr2	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to b \in {Base}_{Y}$
50	1 7 8 41 42 48 49 45	prdsplusgsgrpcl	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to b +_{Y} c \in {Base}_{Y}$
51	1 7 41 42 43 47 50 8	prdsplusgval	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a +_{Y} (b +_{Y} c) = (y \in I ⟼ a (y) +_{R (y)} (b +_{Y} c) (y))$
52	40 46 51	3eqtr4d	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to (a +_{Y} b) +_{Y} c = a +_{Y} (b +_{Y} c)$
53	1	ovexi	$⊢ Y \in V$
54	53	a1i	$⊢ φ \to Y \in V$
55	5 6 17 52 54	issgrpd	$⊢ φ \to Y \in Smgrp$

Metamath Proof Explorer

Theorem prdssgrpd

Proof