Theorem prodsn

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

	Ref	Expression
Hypothesis	prodsn.1	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
Assertion	prodsn	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		prodsn.1	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
2		nfcv	⊢ Ⅎ 𝑚 𝐴
3		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐴
4		csbeq1a	⊢ ( 𝑘 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑘 ⦌ 𝐴 )
5	2 3 4	cbvprodi	⊢ ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ∏ 𝑚 ∈ { 𝑀 } ⦋ 𝑚 / 𝑘 ⦌ 𝐴
6		csbeq1	⊢ ( 𝑚 = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 )
7		1nn	⊢ 1 ∈ ℕ
8	7	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → 1 ∈ ℕ )
9		1z	⊢ 1 ∈ ℤ
10		f1osng	⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ 𝑉 ) → { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } )
11		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
12	9 11	ax-mp	⊢ ( 1 ... 1 ) = { 1 }
13		f1oeq2	⊢ ( ( 1 ... 1 ) = { 1 } → ( { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } ↔ { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } ) )
14	12 13	ax-mp	⊢ ( { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } ↔ { ⟨ 1 , 𝑀 ⟩ } : { 1 } –1-1-onto→ { 𝑀 } )
15	10 14	sylibr	⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ 𝑉 ) → { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } )
16	9 15	mpan	⊢ ( 𝑀 ∈ 𝑉 → { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } )
17	16	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → { ⟨ 1 , 𝑀 ⟩ } : ( 1 ... 1 ) –1-1-onto→ { 𝑀 } )
18		velsn	⊢ ( 𝑚 ∈ { 𝑀 } ↔ 𝑚 = 𝑀 )
19		csbeq1	⊢ ( 𝑚 = 𝑀 → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
20		nfcvd	⊢ ( 𝑀 ∈ 𝑉 → Ⅎ 𝑘 𝐵 )
21	20 1	csbiegf	⊢ ( 𝑀 ∈ 𝑉 → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 = 𝐵 )
22	21	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 = 𝐵 )
23	19 22	sylan9eqr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 = 𝑀 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = 𝐵 )
24	18 23	sylan2b	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = 𝐵 )
25		simplr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → 𝐵 ∈ ℂ )
26	24 25	eqeltrd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑚 ∈ { 𝑀 } ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 ∈ ℂ )
27	12	eleq2i	⊢ ( 𝑛 ∈ ( 1 ... 1 ) ↔ 𝑛 ∈ { 1 } )
28		velsn	⊢ ( 𝑛 ∈ { 1 } ↔ 𝑛 = 1 )
29	27 28	bitri	⊢ ( 𝑛 ∈ ( 1 ... 1 ) ↔ 𝑛 = 1 )
30		fvsng	⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ 𝑉 ) → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) = 𝑀 )
31	9 30	mpan	⊢ ( 𝑀 ∈ 𝑉 → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) = 𝑀 )
32	31	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) = 𝑀 )
33	32	csbeq1d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) / 𝑘 ⦌ 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
34		simpr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
35		fvsng	⊢ ( ( 1 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = 𝐵 )
36	9 34 35	sylancr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = 𝐵 )
37	22 33 36	3eqtr4rd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) / 𝑘 ⦌ 𝐴 )
38		fveq2	⊢ ( 𝑛 = 1 → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) )
39		fveq2	⊢ ( 𝑛 = 1 → ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) )
40	39	csbeq1d	⊢ ( 𝑛 = 1 → ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) / 𝑘 ⦌ 𝐴 )
41	38 40	eqeq12d	⊢ ( 𝑛 = 1 → ( ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 ↔ ( { ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) / 𝑘 ⦌ 𝐴 ) )
42	37 41	syl5ibrcom	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( 𝑛 = 1 → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 ) )
43	42	imp	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 = 1 ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 )
44	29 43	sylan2b	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 1 ... 1 ) ) → ( { ⟨ 1 , 𝐵 ⟩ } ‘ 𝑛 ) = ⦋ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 𝑛 ) / 𝑘 ⦌ 𝐴 )
45	6 8 17 26 44	fprod	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑚 ∈ { 𝑀 } ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ( seq 1 ( · , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) )
46	5 45	syl5eq	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ( seq 1 ( · , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) )
47	9 36	seq1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( seq 1 ( · , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) = 𝐵 )
48	46 47	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )