Theorem prodsnf

Description: A product of a singleton is the term. A version of prodsn using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	prodsnf.1	⊢ Ⅎ 𝑘 𝐵
	prodsnf.2	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
Assertion	prodsnf	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )

Proof

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