Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsmndd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsmndd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsmndd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
Assertion prdsmndd ( 𝜑 → 𝑌 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 prdsmndd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsmndd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3 prdsmndd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdsmndd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
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 ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ Mnd )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
15 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
16 1 7 8 10 12 13 14 15 prdsplusgcl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
17 16 3impb ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
18 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Mnd )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Mnd )
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 mndass ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ Mnd ∧ ( ( 𝑎 ‘ 𝑦 ) ∈ ( 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 ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ Mnd )
49 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
50 1 7 8 41 42 48 49 45 prdsplusgcl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 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 eqid ⊢ ( 0g ∘ 𝑅 ) = ( 0g ∘ 𝑅 )
54 1 7 8 9 11 4 53 prdsidlem ⊢ ( 𝜑 → ( ( 0g ∘ 𝑅 ) ∈ ( Base ‘ 𝑌 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑌 ) ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑎 ) ) )
55 54 simpld ⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) ∈ ( Base ‘ 𝑌 ) )
56 54 simprd ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ 𝑌 ) ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑎 ) )
57 56 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑎 ) )
58 57 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑎 ) = 𝑎 )
59 57 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑎 )
60 5 6 17 52 55 58 59 ismndd ⊢ ( 𝜑 → 𝑌 ∈ Mnd )