prdsmndd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prdsmndd		Structured version Visualization version GIF version

Theorem prdsmndd 18692

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

**Hypotheses**
Ref	Expression
prdsmndd.y	⊢ 𝑌 = (𝑆X_s𝑅)
prdsmndd.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
prdsmndd.s	⊢ (𝜑 → 𝑆 ∈ 𝑉)
prdsmndd.r	⊢ (𝜑 → 𝑅:𝐼⟶Mnd)

**Assertion**
Ref	Expression
prdsmndd	⊢ (𝜑 → 𝑌 ∈ Mnd)

Proof of Theorem prdsmndd Dummy variables 𝑎 𝑏 𝑦 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2731	. 2 ⊢ (𝜑 → (Base‘𝑌) = (Base‘𝑌))
2		eqidd 2731	. 2 ⊢ (𝜑 → (+_g‘𝑌) = (+_g‘𝑌))
3		prdsmndd.y	. . . 4 ⊢ 𝑌 = (𝑆X_s𝑅)
4		eqid 2730	. . . 4 ⊢ (Base‘𝑌) = (Base‘𝑌)
5		eqid 2730	. . . 4 ⊢ (+_g‘𝑌) = (+_g‘𝑌)
6		prdsmndd.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ 𝑉)
7	6	elexd 3493	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ V)
8	7	adantr 479	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑆 ∈ V)
9		prdsmndd.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
10	9	elexd 3493	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ V)
11	10	adantr 479	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝐼 ∈ V)
12		prdsmndd.r	. . . . 5 ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)
13	12	adantr 479	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd)
14		simprl 767	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑌))
15		simprr 769	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌))
16	3, 4, 5, 8, 11, 13, 14, 15	prdsplusgcl 18690	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → (𝑎(+_g‘𝑌)𝑏) ∈ (Base‘𝑌))
17	16	3impb 1113	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌)) → (𝑎(+_g‘𝑌)𝑏) ∈ (Base‘𝑌))
18	12	ffvelcdmda 7085	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Mnd)
19	18	adantlr 711	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Mnd)
20	7	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ V)
21	10	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V)
22	12	ffnd 6717	. . . . . . . 8 ⊢ (𝜑 → 𝑅 Fn 𝐼)
23	22	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼)
24		simplr1 1213	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑌))
25		simpr 483	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼)
26	3, 4, 20, 21, 23, 24, 25	prdsbasprj 17422	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦)))
27		simplr2 1214	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘𝑌))
28	3, 4, 20, 21, 23, 27, 25	prdsbasprj 17422	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦)))
29		simplr3 1215	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑐 ∈ (Base‘𝑌))
30	3, 4, 20, 21, 23, 29, 25	prdsbasprj 17422	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))
31		eqid 2730	. . . . . . 7 ⊢ (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦))
32		eqid 2730	. . . . . . 7 ⊢ (+_g‘(𝑅‘𝑦)) = (+_g‘(𝑅‘𝑦))
33	31, 32	mndass 18668	. . . . . 6 ⊢ (((𝑅‘𝑦) ∈ Mnd ∧ ((𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦)) ∧ (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦)) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → (((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))(𝑏‘𝑦))(+_g‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦))))
34	19, 26, 28, 30, 33	syl13anc 1370	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))(𝑏‘𝑦))(+_g‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦))))
35	3, 4, 20, 21, 23, 24, 27, 5, 25	prdsplusgfval 17424	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+_g‘𝑌)𝑏)‘𝑦) = ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))(𝑏‘𝑦)))
36	35	oveq1d 7426	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎(+_g‘𝑌)𝑏)‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦)) = (((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))(𝑏‘𝑦))(+_g‘(𝑅‘𝑦))(𝑐‘𝑦)))
37	3, 4, 20, 21, 23, 27, 29, 5, 25	prdsplusgfval 17424	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑏(+_g‘𝑌)𝑐)‘𝑦) = ((𝑏‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦)))
38	37	oveq2d 7427	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏(+_g‘𝑌)𝑐)‘𝑦)) = ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦))))
39	34, 36, 38	3eqtr4d 2780	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎(+_g‘𝑌)𝑏)‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏(+_g‘𝑌)𝑐)‘𝑦)))
40	39	mpteq2dva 5247	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ (((𝑎(+_g‘𝑌)𝑏)‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦))) = (𝑦 ∈ 𝐼 ↦ ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏(+_g‘𝑌)𝑐)‘𝑦))))
41	7	adantr 479	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ V)
42	10	adantr 479	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V)
43	22	adantr 479	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼)
44	16	3adantr3 1169	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(+_g‘𝑌)𝑏) ∈ (Base‘𝑌))
45		simpr3 1194	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌))
46	3, 4, 41, 42, 43, 44, 45, 5	prdsplusgval 17423	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+_g‘𝑌)𝑏)(+_g‘𝑌)𝑐) = (𝑦 ∈ 𝐼 ↦ (((𝑎(+_g‘𝑌)𝑏)‘𝑦)(+_g‘(𝑅‘𝑦))(𝑐‘𝑦))))
47		simpr1 1192	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑌))
48	12	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd)
49		simpr2 1193	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌))
50	3, 4, 5, 41, 42, 48, 49, 45	prdsplusgcl 18690	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑏(+_g‘𝑌)𝑐) ∈ (Base‘𝑌))
51	3, 4, 41, 42, 43, 47, 50, 5	prdsplusgval 17423	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(+_g‘𝑌)(𝑏(+_g‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ ((𝑎‘𝑦)(+_g‘(𝑅‘𝑦))((𝑏(+_g‘𝑌)𝑐)‘𝑦))))
52	40, 46, 51	3eqtr4d 2780	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+_g‘𝑌)𝑏)(+_g‘𝑌)𝑐) = (𝑎(+_g‘𝑌)(𝑏(+_g‘𝑌)𝑐)))
53		eqid 2730	. . . 4 ⊢ (0_g ∘ 𝑅) = (0_g ∘ 𝑅)
54	3, 4, 5, 7, 10, 12, 53	prdsidlem 18691	. . 3 ⊢ (𝜑 → ((0_g ∘ 𝑅) ∈ (Base‘𝑌) ∧ ∀𝑎 ∈ (Base‘𝑌)(((0_g ∘ 𝑅)(+_g‘𝑌)𝑎) = 𝑎 ∧ (𝑎(+_g‘𝑌)(0_g ∘ 𝑅)) = 𝑎)))
55	54	simpld 493	. 2 ⊢ (𝜑 → (0_g ∘ 𝑅) ∈ (Base‘𝑌))
56	54	simprd 494	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ (Base‘𝑌)(((0_g ∘ 𝑅)(+_g‘𝑌)𝑎) = 𝑎 ∧ (𝑎(+_g‘𝑌)(0_g ∘ 𝑅)) = 𝑎))
57	56	r19.21bi 3246	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (((0_g ∘ 𝑅)(+_g‘𝑌)𝑎) = 𝑎 ∧ (𝑎(+_g‘𝑌)(0_g ∘ 𝑅)) = 𝑎))
58	57	simpld 493	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ((0_g ∘ 𝑅)(+_g‘𝑌)𝑎) = 𝑎)
59	57	simprd 494	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (𝑎(+_g‘𝑌)(0_g ∘ 𝑅)) = 𝑎)
60	1, 2, 17, 52, 55, 58, 59	ismndd 18681	1 ⊢ (𝜑 → 𝑌 ∈ Mnd)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ∀wral 3059 Vcvv 3472 ↦ cmpt 5230 ∘ ccom 5679 Fn wfn 6537 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 Basecbs 17148 +_gcplusg 17201 0_gc0g 17389 X_scprds 17395 Mndcmnd 18659

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-fz 13489 df-struct 17084 df-slot 17119 df-ndx 17131 df-base 17149 df-plusg 17214 df-mulr 17215 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ds 17223 df-hom 17225 df-cco 17226 df-0g 17391 df-prds 17397 df-mgm 18565 df-sgrp 18644 df-mnd 18660

This theorem is referenced by: prds0g 18693 pwsmnd 18694 xpsmnd 18699 prdspjmhm 18746 prdsgrpd 18969 prdscmnd 19770 prdsringd 20209 dsmm0cl 21514 prdstmdd 23848

W3C validator