prdsmndd

Description: The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		prdsmndd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsmndd.i	$⊢ φ \to I \in W$
3		prdsmndd.s	$⊢ φ \to S \in V$
4		prdsmndd.r	$⊢ φ \to R : I ⟶ Mnd$
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 ⟶ Mnd$
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	prdsplusgcl	$⊢ (φ \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	ffvelrnda	$⊢ (φ \land y \in I) \to R (y) \in Mnd$
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 Mnd$
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	mndass	$⊢ (R (y) \in Mnd \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 ⟶ Mnd$
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	prdsplusgcl	$⊢ (φ \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		eqid	$⊢ 0_{𝑔} \circ R = 0_{𝑔} \circ R$
54	1 7 8 9 11 4 53	prdsidlem	$⊢ φ \to (0_{𝑔} \circ R \in {Base}_{Y} \land \forall a \in {Base}_{Y} ((0_{𝑔} \circ R) +_{Y} a = a \land a +_{Y} (0_{𝑔} \circ R) = a))$
55	54	simpld	$⊢ φ \to 0_{𝑔} \circ R \in {Base}_{Y}$
56	54	simprd	$⊢ φ \to \forall a \in {Base}_{Y} ((0_{𝑔} \circ R) +_{Y} a = a \land a +_{Y} (0_{𝑔} \circ R) = a)$
57	56	r19.21bi	$⊢ (φ \land a \in {Base}_{Y}) \to ((0_{𝑔} \circ R) +_{Y} a = a \land a +_{Y} (0_{𝑔} \circ R) = a)$
58	57	simpld	$⊢ (φ \land a \in {Base}_{Y}) \to (0_{𝑔} \circ R) +_{Y} a = a$
59	57	simprd	$⊢ (φ \land a \in {Base}_{Y}) \to a +_{Y} (0_{𝑔} \circ R) = a$
60	5 6 17 52 55 58 59	ismndd	$⊢ φ \to Y \in Mnd$

Metamath Proof Explorer

Theorem prdsmndd

Proof