Metamath Proof Explorer


Theorem prdsplusgcl

Description: Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsplusgcl.y 𝑌 = ( 𝑆 Xs 𝑅 )
prdsplusgcl.b 𝐵 = ( Base ‘ 𝑌 )
prdsplusgcl.p + = ( +g𝑌 )
prdsplusgcl.s ( 𝜑𝑆𝑉 )
prdsplusgcl.i ( 𝜑𝐼𝑊 )
prdsplusgcl.r ( 𝜑𝑅 : 𝐼 ⟶ Mnd )
prdsplusgcl.f ( 𝜑𝐹𝐵 )
prdsplusgcl.g ( 𝜑𝐺𝐵 )
Assertion prdsplusgcl ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 prdsplusgcl.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsplusgcl.b 𝐵 = ( Base ‘ 𝑌 )
3 prdsplusgcl.p + = ( +g𝑌 )
4 prdsplusgcl.s ( 𝜑𝑆𝑉 )
5 prdsplusgcl.i ( 𝜑𝐼𝑊 )
6 prdsplusgcl.r ( 𝜑𝑅 : 𝐼 ⟶ Mnd )
7 prdsplusgcl.f ( 𝜑𝐹𝐵 )
8 prdsplusgcl.g ( 𝜑𝐺𝐵 )
9 6 ffnd ( 𝜑𝑅 Fn 𝐼 )
10 1 2 4 5 9 7 8 3 prdsplusgval ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) )
11 6 ffvelrnda ( ( 𝜑𝑥𝐼 ) → ( 𝑅𝑥 ) ∈ Mnd )
12 4 adantr ( ( 𝜑𝑥𝐼 ) → 𝑆𝑉 )
13 5 adantr ( ( 𝜑𝑥𝐼 ) → 𝐼𝑊 )
14 9 adantr ( ( 𝜑𝑥𝐼 ) → 𝑅 Fn 𝐼 )
15 7 adantr ( ( 𝜑𝑥𝐼 ) → 𝐹𝐵 )
16 simpr ( ( 𝜑𝑥𝐼 ) → 𝑥𝐼 )
17 1 2 12 13 14 15 16 prdsbasprj ( ( 𝜑𝑥𝐼 ) → ( 𝐹𝑥 ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) )
18 8 adantr ( ( 𝜑𝑥𝐼 ) → 𝐺𝐵 )
19 1 2 12 13 14 18 16 prdsbasprj ( ( 𝜑𝑥𝐼 ) → ( 𝐺𝑥 ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) )
20 eqid ( Base ‘ ( 𝑅𝑥 ) ) = ( Base ‘ ( 𝑅𝑥 ) )
21 eqid ( +g ‘ ( 𝑅𝑥 ) ) = ( +g ‘ ( 𝑅𝑥 ) )
22 20 21 mndcl ( ( ( 𝑅𝑥 ) ∈ Mnd ∧ ( 𝐹𝑥 ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) ∧ ( 𝐺𝑥 ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) ) → ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) )
23 11 17 19 22 syl3anc ( ( 𝜑𝑥𝐼 ) → ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) )
24 23 ralrimiva ( 𝜑 → ∀ 𝑥𝐼 ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) )
25 1 2 4 5 9 prdsbasmpt ( 𝜑 → ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∈ 𝐵 ↔ ∀ 𝑥𝐼 ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ∈ ( Base ‘ ( 𝑅𝑥 ) ) ) )
26 24 25 mpbird ( 𝜑 → ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∈ 𝐵 )
27 10 26 eqeltrd ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )