This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )