Metamath Proof Explorer


Theorem fprodcllemf

Description: Finite product closure lemma. A version of fprodcllem using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodcllemf.ph 𝑘 𝜑
fprodcllemf.s ( 𝜑𝑆 ⊆ ℂ )
fprodcllemf.xy ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
fprodcllemf.a ( 𝜑𝐴 ∈ Fin )
fprodcllemf.b ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
fprodcllemf.1 ( 𝜑 → 1 ∈ 𝑆 )
Assertion fprodcllemf ( 𝜑 → ∏ 𝑘𝐴 𝐵𝑆 )

Proof

Step Hyp Ref Expression
1 fprodcllemf.ph 𝑘 𝜑
2 fprodcllemf.s ( 𝜑𝑆 ⊆ ℂ )
3 fprodcllemf.xy ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
4 fprodcllemf.a ( 𝜑𝐴 ∈ Fin )
5 fprodcllemf.b ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
6 fprodcllemf.1 ( 𝜑 → 1 ∈ 𝑆 )
7 nfcv 𝑗 𝐵
8 nfcsb1v 𝑘 𝑗 / 𝑘 𝐵
9 csbeq1a ( 𝑘 = 𝑗𝐵 = 𝑗 / 𝑘 𝐵 )
10 7 8 9 cbvprodi 𝑘𝐴 𝐵 = ∏ 𝑗𝐴 𝑗 / 𝑘 𝐵
11 5 ex ( 𝜑 → ( 𝑘𝐴𝐵𝑆 ) )
12 1 11 ralrimi ( 𝜑 → ∀ 𝑘𝐴 𝐵𝑆 )
13 rspsbc ( 𝑗𝐴 → ( ∀ 𝑘𝐴 𝐵𝑆[ 𝑗 / 𝑘 ] 𝐵𝑆 ) )
14 12 13 mpan9 ( ( 𝜑𝑗𝐴 ) → [ 𝑗 / 𝑘 ] 𝐵𝑆 )
15 sbcel1g ( 𝑗 ∈ V → ( [ 𝑗 / 𝑘 ] 𝐵𝑆 𝑗 / 𝑘 𝐵𝑆 ) )
16 15 elv ( [ 𝑗 / 𝑘 ] 𝐵𝑆 𝑗 / 𝑘 𝐵𝑆 )
17 14 16 sylib ( ( 𝜑𝑗𝐴 ) → 𝑗 / 𝑘 𝐵𝑆 )
18 2 3 4 17 6 fprodcllem ( 𝜑 → ∏ 𝑗𝐴 𝑗 / 𝑘 𝐵𝑆 )
19 10 18 eqeltrid ( 𝜑 → ∏ 𝑘𝐴 𝐵𝑆 )