Metamath Proof Explorer

Theorem prdssgrpd

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

Ref Expression
Hypotheses prdssgrpd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdssgrpd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdssgrpd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdssgrpd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Smgrp )
Assertion prdssgrpd ( 𝜑 → 𝑌 ∈ Smgrp )

Proof

Step Hyp Ref Expression
1 prdssgrpd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdssgrpd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3 prdssgrpd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdssgrpd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Smgrp )
5 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
6 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) )
7 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
8 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
9 3 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
10 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ V )
11 2 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ Smgrp )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
15 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
16 1 7 8 10 12 13 14 15 prdsplusgsgrpcl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
17 16 3impb ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
18 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Smgrp )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Smgrp )
20 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ V )
21 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
22 4 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
24 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
25 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
26 1 7 20 21 23 24 25 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
27 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
28 1 7 20 21 23 27 25 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
29 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
30 1 7 20 21 23 29 25 prdsbasprj ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
31 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
32 eqid ⊢ ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑦 ) )
33 31 32 sgrpass ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ Smgrp ∧ ( ( 𝑎 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
34 19 26 28 30 33 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
35 1 7 20 21 23 24 27 8 25 prdsplusgfval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) = ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) )
36 35 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
37 1 7 20 21 23 27 29 8 25 prdsplusgfval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
38 37 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
39 34 36 38 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
40 39 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
41 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ V )
42 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
43 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 Fn 𝐼 )
44 16 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
45 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
46 1 7 41 42 43 44 45 8 prdsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( +g ‘ 𝑌 ) 𝑐 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
47 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
48 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ Smgrp )
49 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
50 1 7 8 41 42 48 49 45 prdsplusgsgrpcl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
51 1 7 41 42 43 47 50 8 prdsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( +g ‘ 𝑌 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
52 40 46 51 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( +g ‘ 𝑌 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑌 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) )
53 1 ovexi ⊢ 𝑌 ∈ V
54 53 a1i ⊢ ( 𝜑 → 𝑌 ∈ V )
55 5 6 17 52 54 issgrpd ⊢ ( 𝜑 → 𝑌 ∈ Smgrp )