Metamath Proof Explorer

Theorem prdsmulrngcl

Description: Closure of the multiplication in a structure product of non-unital rings. (Contributed by Mario Carneiro, 11-Mar-2015) Generalization of prdsmulrcl . (Revised by AV, 21-Feb-2025)

Ref Expression
Hypotheses prdsmulrngcl.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsmulrngcl.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsmulrngcl.t ⊢ · = ( .r ‘ 𝑌 )
prdsmulrngcl.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsmulrngcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsmulrngcl.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Rng )
prdsmulrngcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
prdsmulrngcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion prdsmulrngcl ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 prdsmulrngcl.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsmulrngcl.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsmulrngcl.t ⊢ · = ( .r ‘ 𝑌 )
4 prdsmulrngcl.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5 prdsmulrngcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 prdsmulrngcl.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Rng )
7 prdsmulrngcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8 prdsmulrngcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9 6 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
10 1 2 4 5 9 7 8 3 prdsmulrval ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
11 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ Rng )
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 ⊢ ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) = ( .r ‘ ( 𝑅 ‘ 𝑥 ) )
22 20 21 rngcl ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ Rng ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
23 11 17 19 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
25 1 2 4 5 9 prdsbasmpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
26 24 25 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ 𝐵 )
27 10 26 eqeltrd ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )