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

Metamath Proof Explorer

Theorem prodsns

Description: A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017)

Ref Expression
Assertion prodsns ⊢ M ∈ V ∧ ⦋ M / k⦌ A ∈ ℂ → ∏ k ∈ M A = ⦋ M / k⦌ A

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ n A
2 nfcsb1v ⊢ Ⅎ _ k ⦋ n / k⦌ A
3 csbeq1a ⊢ k = n → A = ⦋ n / k⦌ A
4 1 2 3 cbvprodi ⊢ ∏ k ∈ M A = ∏ n ∈ M ⦋ n / k⦌ A
5 csbeq1 ⊢ n = M → ⦋ n / k⦌ A = ⦋ M / k⦌ A
6 5 prodsn ⊢ M ∈ V ∧ ⦋ M / k⦌ A ∈ ℂ → ∏ n ∈ M ⦋ n / k⦌ A = ⦋ M / k⦌ A
7 4 6 eqtrid ⊢ M ∈ V ∧ ⦋ M / k⦌ A ∈ ℂ → ∏ k ∈ M A = ⦋ M / k⦌ A