prdsringd

Description: A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		prdsringd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsringd.i	$⊢ φ \to I \in W$
3		prdsringd.s	$⊢ φ \to S \in V$
4		prdsringd.r	$⊢ φ \to R : I ⟶ Ring$
5		ringgrp	$⊢ x \in Ring \to x \in Grp$
6	5	ssriv	$⊢ Ring \subseteq Grp$
7		fss	$⊢ (R : I ⟶ Ring \land Ring \subseteq Grp) \to R : I ⟶ Grp$
8	4 6 7	sylancl	$⊢ φ \to R : I ⟶ Grp$
9	1 2 3 8	prdsgrpd	$⊢ φ \to Y \in Grp$
10		eqid	$⊢ S ⨉_{𝑠} (mulGrp \circ R) = S ⨉_{𝑠} (mulGrp \circ R)$
11		mgpf	$⊢ ({mulGrp ↾}_{Ring}) : Ring ⟶ Mnd$
12		fco2	$⊢ (({mulGrp ↾}_{Ring}) : Ring ⟶ Mnd \land R : I ⟶ Ring) \to (mulGrp \circ R) : I ⟶ Mnd$
13	11 4 12	sylancr	$⊢ φ \to (mulGrp \circ R) : I ⟶ Mnd$
14	10 2 3 13	prdsmndd	$⊢ φ \to S ⨉_{𝑠} (mulGrp \circ R) \in Mnd$
15		eqidd	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
16		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
17	4	ffnd	$⊢ φ \to R Fn I$
18	1 16 10 2 3 17	prdsmgp	$⊢ φ \to ({Base}_{{mulGrp}_{Y}} = {Base}_{(S ⨉_{𝑠} (mulGrp \circ R))} \land +_{{mulGrp}_{Y}} = +_{(S ⨉_{𝑠} (mulGrp \circ R))})$
19	18	simpld	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{(S ⨉_{𝑠} (mulGrp \circ R))}$
20	18	simprd	$⊢ φ \to +_{{mulGrp}_{Y}} = +_{(S ⨉_{𝑠} (mulGrp \circ R))}$
21	20	oveqdr	$⊢ (φ \land (x \in {Base}_{{mulGrp}_{Y}} \land y \in {Base}_{{mulGrp}_{Y}})) \to x +_{{mulGrp}_{Y}} y = x +_{(S ⨉_{𝑠} (mulGrp \circ R))} y$
22	15 19 21	mndpropd	$⊢ φ \to ({mulGrp}_{Y} \in Mnd \leftrightarrow S ⨉_{𝑠} (mulGrp \circ R) \in Mnd)$
23	14 22	mpbird	$⊢ φ \to {mulGrp}_{Y} \in Mnd$
24	4	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to R : I ⟶ Ring$
25	24	ffvelrnda	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to R (w) \in Ring$
26		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
27	3	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to S \in V$
28	27	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to S \in V$
29	2	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to I \in W$
30	29	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to I \in W$
31	17	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to R Fn I$
32	31	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to R Fn I$
33		simplr1	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to x \in {Base}_{Y}$
34		simpr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to w \in I$
35	1 26 28 30 32 33 34	prdsbasprj	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to x (w) \in {Base}_{R (w)}$
36		simpr2	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to y \in {Base}_{Y}$
37	36	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to y \in {Base}_{Y}$
38	1 26 28 30 32 37 34	prdsbasprj	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to y (w) \in {Base}_{R (w)}$
39		simpr3	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to z \in {Base}_{Y}$
40	39	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to z \in {Base}_{Y}$
41	1 26 28 30 32 40 34	prdsbasprj	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to z (w) \in {Base}_{R (w)}$
42		eqid	$⊢ {Base}_{R (w)} = {Base}_{R (w)}$
43		eqid	$⊢ +_{R (w)} = +_{R (w)}$
44		eqid	$⊢ \cdot_{R (w)} = \cdot_{R (w)}$
45	42 43 44	ringdi	$⊢ (R (w) \in Ring \land (x (w) \in {Base}_{R (w)} \land y (w) \in {Base}_{R (w)} \land z (w) \in {Base}_{R (w)})) \to x (w) \cdot_{R (w)} (y (w) +_{R (w)} z (w)) = (x (w) \cdot_{R (w)} y (w)) +_{R (w)} (x (w) \cdot_{R (w)} z (w))$
46	25 35 38 41 45	syl13anc	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to x (w) \cdot_{R (w)} (y (w) +_{R (w)} z (w)) = (x (w) \cdot_{R (w)} y (w)) +_{R (w)} (x (w) \cdot_{R (w)} z (w))$
47		eqid	$⊢ +_{Y} = +_{Y}$
48	1 26 28 30 32 37 40 47 34	prdsplusgfval	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (y +_{Y} z) (w) = y (w) +_{R (w)} z (w)$
49	48	oveq2d	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to x (w) \cdot_{R (w)} (y +_{Y} z) (w) = x (w) \cdot_{R (w)} (y (w) +_{R (w)} z (w))$
50		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
51	1 26 28 30 32 33 37 50 34	prdsmulrfval	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x \cdot_{Y} y) (w) = x (w) \cdot_{R (w)} y (w)$
52	1 26 28 30 32 33 40 50 34	prdsmulrfval	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x \cdot_{Y} z) (w) = x (w) \cdot_{R (w)} z (w)$
53	51 52	oveq12d	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x \cdot_{Y} y) (w) +_{R (w)} (x \cdot_{Y} z) (w) = (x (w) \cdot_{R (w)} y (w)) +_{R (w)} (x (w) \cdot_{R (w)} z (w))$
54	46 49 53	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to x (w) \cdot_{R (w)} (y +_{Y} z) (w) = (x \cdot_{Y} y) (w) +_{R (w)} (x \cdot_{Y} z) (w)$
55	54	mpteq2dva	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (w \in I ⟼ x (w) \cdot_{R (w)} (y +_{Y} z) (w)) = (w \in I ⟼ (x \cdot_{Y} y) (w) +_{R (w)} (x \cdot_{Y} z) (w))$
56		simpr1	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \in {Base}_{Y}$
57		ringmnd	$⊢ x \in Ring \to x \in Mnd$
58	57	ssriv	$⊢ Ring \subseteq Mnd$
59		fss	$⊢ (R : I ⟶ Ring \land Ring \subseteq Mnd) \to R : I ⟶ Mnd$
60	4 58 59	sylancl	$⊢ φ \to R : I ⟶ Mnd$
61	60	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to R : I ⟶ Mnd$
62	1 26 47 27 29 61 36 39	prdsplusgcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to y +_{Y} z \in {Base}_{Y}$
63	1 26 27 29 31 56 62 50	prdsmulrval	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \cdot_{Y} (y +_{Y} z) = (w \in I ⟼ x (w) \cdot_{R (w)} (y +_{Y} z) (w))$
64	1 26 50 27 29 24 56 36	prdsmulrcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \cdot_{Y} y \in {Base}_{Y}$
65	1 26 50 27 29 24 56 39	prdsmulrcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \cdot_{Y} z \in {Base}_{Y}$
66	1 26 27 29 31 64 65 47	prdsplusgval	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (x \cdot_{Y} y) +_{Y} (x \cdot_{Y} z) = (w \in I ⟼ (x \cdot_{Y} y) (w) +_{R (w)} (x \cdot_{Y} z) (w))$
67	55 63 66	3eqtr4d	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \cdot_{Y} (y +_{Y} z) = (x \cdot_{Y} y) +_{Y} (x \cdot_{Y} z)$
68	42 43 44	ringdir	$⊢ (R (w) \in Ring \land (x (w) \in {Base}_{R (w)} \land y (w) \in {Base}_{R (w)} \land z (w) \in {Base}_{R (w)})) \to (x (w) +_{R (w)} y (w)) \cdot_{R (w)} z (w) = (x (w) \cdot_{R (w)} z (w)) +_{R (w)} (y (w) \cdot_{R (w)} z (w))$
69	25 35 38 41 68	syl13anc	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x (w) +_{R (w)} y (w)) \cdot_{R (w)} z (w) = (x (w) \cdot_{R (w)} z (w)) +_{R (w)} (y (w) \cdot_{R (w)} z (w))$
70	1 26 28 30 32 33 37 47 34	prdsplusgfval	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x +_{Y} y) (w) = x (w) +_{R (w)} y (w)$
71	70	oveq1d	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x +_{Y} y) (w) \cdot_{R (w)} z (w) = (x (w) +_{R (w)} y (w)) \cdot_{R (w)} z (w)$
72	1 26 28 30 32 37 40 50 34	prdsmulrfval	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (y \cdot_{Y} z) (w) = y (w) \cdot_{R (w)} z (w)$
73	52 72	oveq12d	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x \cdot_{Y} z) (w) +_{R (w)} (y \cdot_{Y} z) (w) = (x (w) \cdot_{R (w)} z (w)) +_{R (w)} (y (w) \cdot_{R (w)} z (w))$
74	69 71 73	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to (x +_{Y} y) (w) \cdot_{R (w)} z (w) = (x \cdot_{Y} z) (w) +_{R (w)} (y \cdot_{Y} z) (w)$
75	74	mpteq2dva	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (w \in I ⟼ (x +_{Y} y) (w) \cdot_{R (w)} z (w)) = (w \in I ⟼ (x \cdot_{Y} z) (w) +_{R (w)} (y \cdot_{Y} z) (w))$
76	1 26 47 27 29 61 56 36	prdsplusgcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x +_{Y} y \in {Base}_{Y}$
77	1 26 27 29 31 76 39 50	prdsmulrval	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (x +_{Y} y) \cdot_{Y} z = (w \in I ⟼ (x +_{Y} y) (w) \cdot_{R (w)} z (w))$
78	1 26 50 27 29 24 36 39	prdsmulrcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to y \cdot_{Y} z \in {Base}_{Y}$
79	1 26 27 29 31 65 78 47	prdsplusgval	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (x \cdot_{Y} z) +_{Y} (y \cdot_{Y} z) = (w \in I ⟼ (x \cdot_{Y} z) (w) +_{R (w)} (y \cdot_{Y} z) (w))$
80	75 77 79	3eqtr4d	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (x +_{Y} y) \cdot_{Y} z = (x \cdot_{Y} z) +_{Y} (y \cdot_{Y} z)$
81	67 80	jca	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to (x \cdot_{Y} (y +_{Y} z) = (x \cdot_{Y} y) +_{Y} (x \cdot_{Y} z) \land (x +_{Y} y) \cdot_{Y} z = (x \cdot_{Y} z) +_{Y} (y \cdot_{Y} z))$
82	81	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{Y} \forall y \in {Base}_{Y} \forall z \in {Base}_{Y} (x \cdot_{Y} (y +_{Y} z) = (x \cdot_{Y} y) +_{Y} (x \cdot_{Y} z) \land (x +_{Y} y) \cdot_{Y} z = (x \cdot_{Y} z) +_{Y} (y \cdot_{Y} z))$
83	26 16 47 50	isring	$⊢ Y \in Ring \leftrightarrow (Y \in Grp \land {mulGrp}_{Y} \in Mnd \land \forall x \in {Base}_{Y} \forall y \in {Base}_{Y} \forall z \in {Base}_{Y} (x \cdot_{Y} (y +_{Y} z) = (x \cdot_{Y} y) +_{Y} (x \cdot_{Y} z) \land (x +_{Y} y) \cdot_{Y} z = (x \cdot_{Y} z) +_{Y} (y \cdot_{Y} z)))$
84	9 23 82 83	syl3anbrc	$⊢ φ \to Y \in Ring$

Metamath Proof Explorer

Theorem prdsringd

Proof