Theorem prodsns

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

	Ref	Expression
Assertion	prodsns	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑛 𝐴
2		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐴
3		csbeq1a	⊢ ( 𝑘 = 𝑛 → 𝐴 = ⦋ 𝑛 / 𝑘 ⦌ 𝐴 )
4	1 2 3	cbvprodi	⊢ ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ∏ 𝑛 ∈ { 𝑀 } ⦋ 𝑛 / 𝑘 ⦌ 𝐴
5		csbeq1	⊢ ( 𝑛 = 𝑀 → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
6	5	prodsn	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ∏ 𝑛 ∈ { 𝑀 } ⦋ 𝑛 / 𝑘 ⦌ 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
7	4 6	eqtrid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )