prdsrngd

Description: A product of non-unital rings is a non-unital ring. (Contributed by AV, 22-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		prdsrngd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsrngd.i	$⊢ φ \to I \in W$
3		prdsrngd.s	$⊢ φ \to S \in V$
4		prdsrngd.r	$⊢ φ \to R : I ⟶ Rng$
5		rngabl	$⊢ x \in Rng \to x \in Abel$
6	5	ssriv	$⊢ Rng \subseteq Abel$
7		fss	$⊢ (R : I ⟶ Rng \land Rng \subseteq Abel) \to R : I ⟶ Abel$
8	4 6 7	sylancl	$⊢ φ \to R : I ⟶ Abel$
9	1 2 3 8	prdsabld	$⊢ φ \to Y \in Abel$
10		eqid	$⊢ S ⨉_{𝑠} (mulGrp \circ R) = S ⨉_{𝑠} (mulGrp \circ R)$
11		rngmgpf	$⊢ ({mulGrp ↾}_{Rng}) : Rng ⟶ Smgrp$
12		fco2	$⊢ (({mulGrp ↾}_{Rng}) : Rng ⟶ Smgrp \land R : I ⟶ Rng) \to (mulGrp \circ R) : I ⟶ Smgrp$
13	11 4 12	sylancr	$⊢ φ \to (mulGrp \circ R) : I ⟶ Smgrp$
14	10 2 3 13	prdssgrpd	$⊢ φ \to S ⨉_{𝑠} (mulGrp \circ R) \in Smgrp$
15		fvexd	$⊢ φ \to {mulGrp}_{Y} \in V$
16		ovexd	$⊢ φ \to S ⨉_{𝑠} (mulGrp \circ R) \in V$
17		eqidd	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
18		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
19	4	ffnd	$⊢ φ \to R Fn I$
20	1 18 10 2 3 19	prdsmgp	$⊢ φ \to ({Base}_{{mulGrp}_{Y}} = {Base}_{(S ⨉_{𝑠} (mulGrp \circ R))} \land +_{{mulGrp}_{Y}} = +_{(S ⨉_{𝑠} (mulGrp \circ R))})$
21	20	simpld	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{(S ⨉_{𝑠} (mulGrp \circ R))}$
22	20	simprd	$⊢ φ \to +_{{mulGrp}_{Y}} = +_{(S ⨉_{𝑠} (mulGrp \circ R))}$
23	22	oveqdr	$⊢ (φ \land (x \in {Base}_{{mulGrp}_{Y}} \land y \in {Base}_{{mulGrp}_{Y}})) \to x +_{{mulGrp}_{Y}} y = x +_{(S ⨉_{𝑠} (mulGrp \circ R))} y$
24	15 16 17 21 23	sgrppropd	$⊢ φ \to ({mulGrp}_{Y} \in Smgrp \leftrightarrow S ⨉_{𝑠} (mulGrp \circ R) \in Smgrp)$
25	14 24	mpbird	$⊢ φ \to {mulGrp}_{Y} \in Smgrp$
26	4	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to R : I ⟶ Rng$
27	26	ffvelcdmda	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to R (w) \in Rng$
28		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
29	3	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to S \in V$
30	29	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to S \in V$
31	2	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to I \in W$
32	31	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to I \in W$
33	19	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to R Fn I$
34	33	adantr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to R Fn I$
35		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}$
36		simpr	$⊢ ((φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \land w \in I) \to w \in I$
37	1 28 30 32 34 35 36	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)}$
38		simpr2	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to y \in {Base}_{Y}$
39	38	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}$
40	1 28 30 32 34 39 36	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)}$
41		simpr3	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to z \in {Base}_{Y}$
42	41	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}$
43	1 28 30 32 34 42 36	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)}$
44		eqid	$⊢ {Base}_{R (w)} = {Base}_{R (w)}$
45		eqid	$⊢ +_{R (w)} = +_{R (w)}$
46		eqid	$⊢ \cdot_{R (w)} = \cdot_{R (w)}$
47	44 45 46	rngdi	$⊢ (R (w) \in Rng \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))$
48	27 37 40 43 47	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))$
49		eqid	$⊢ +_{Y} = +_{Y}$
50	1 28 30 32 34 39 42 49 36	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)$
51	50	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))$
52		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
53	1 28 30 32 34 35 39 52 36	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)$
54	1 28 30 32 34 35 42 52 36	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)$
55	53 54	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))$
56	48 51 55	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)$
57	56	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))$
58		simpr1	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \in {Base}_{Y}$
59		rnggrp	$⊢ x \in Rng \to x \in Grp$
60	59	grpmndd	$⊢ x \in Rng \to x \in Mnd$
61	60	ssriv	$⊢ Rng \subseteq Mnd$
62		fss	$⊢ (R : I ⟶ Rng \land Rng \subseteq Mnd) \to R : I ⟶ Mnd$
63	4 61 62	sylancl	$⊢ φ \to R : I ⟶ Mnd$
64	63	adantr	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to R : I ⟶ Mnd$
65	1 28 49 29 31 64 38 41	prdsplusgcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to y +_{Y} z \in {Base}_{Y}$
66	1 28 29 31 33 58 65 52	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))$
67	1 28 52 29 31 26 58 38	prdsmulrngcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \cdot_{Y} y \in {Base}_{Y}$
68	1 28 52 29 31 26 58 41	prdsmulrngcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x \cdot_{Y} z \in {Base}_{Y}$
69	1 28 29 31 33 67 68 49	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))$
70	57 66 69	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)$
71	44 45 46	rngdir	$⊢ (R (w) \in Rng \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))$
72	27 37 40 43 71	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))$
73	1 28 30 32 34 35 39 49 36	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)$
74	73	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)$
75	1 28 30 32 34 39 42 52 36	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)$
76	54 75	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))$
77	72 74 76	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)$
78	77	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))$
79	1 28 49 29 31 64 58 38	prdsplusgcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to x +_{Y} y \in {Base}_{Y}$
80	1 28 29 31 33 79 41 52	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))$
81	1 28 52 29 31 26 38 41	prdsmulrngcl	$⊢ (φ \land (x \in {Base}_{Y} \land y \in {Base}_{Y} \land z \in {Base}_{Y})) \to y \cdot_{Y} z \in {Base}_{Y}$
82	1 28 29 31 33 68 81 49	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))$
83	78 80 82	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)$
84	70 83	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))$
85	84	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))$
86	28 18 49 52	isrng	$⊢ Y \in Rng \leftrightarrow (Y \in Abel \land {mulGrp}_{Y} \in Smgrp \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)))$
87	9 25 85 86	syl3anbrc	$⊢ φ \to Y \in Rng$

Metamath Proof Explorer

Theorem prdsrngd

Proof