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	|- F/_ k B
	prodsnf.2	|- ( k = M -> A = B )
Assertion	prodsnf	|- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )

Proof

Step	Hyp	Ref	Expression
1		prodsnf.1	|- F/_ k B
2		prodsnf.2	|- ( k = M -> A = B )
3		nfcv	|- F/_ m A
4		nfcsb1v	|- F/_ k [_ m / k ]_ A
5		csbeq1a	|- ( k = m -> A = [_ m / k ]_ A )
6	3 4 5	cbvprodi	|- prod_ k e. { M } A = prod_ m e. { M } [_ m / k ]_ A
7		csbeq1	|- ( m = ( { <. 1 , M >. } ` n ) -> [_ m / k ]_ A = [_ ( { <. 1 , M >. } ` n ) / k ]_ A )
8		1nn	|- 1 e. NN
9	8	a1i	|- ( ( M e. V /\ B e. CC ) -> 1 e. NN )
10		1z	|- 1 e. ZZ
11		f1osng	|- ( ( 1 e. ZZ /\ M e. V ) -> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } )
12		fzsn	|- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
13	10 12	ax-mp	|- ( 1 ... 1 ) = { 1 }
14		f1oeq2	|- ( ( 1 ... 1 ) = { 1 } -> ( { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } <-> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } ) )
15	13 14	ax-mp	|- ( { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } <-> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } )
16	11 15	sylibr	|- ( ( 1 e. ZZ /\ M e. V ) -> { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } )
17	10 16	mpan	|- ( M e. V -> { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } )
18	17	adantr	|- ( ( M e. V /\ B e. CC ) -> { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } )
19		velsn	|- ( m e. { M } <-> m = M )
20		csbeq1	|- ( m = M -> [_ m / k ]_ A = [_ M / k ]_ A )
21	1	a1i	|- ( M e. V -> F/_ k B )
22	21 2	csbiegf	|- ( M e. V -> [_ M / k ]_ A = B )
23	22	adantr	|- ( ( M e. V /\ B e. CC ) -> [_ M / k ]_ A = B )
24	20 23	sylan9eqr	|- ( ( ( M e. V /\ B e. CC ) /\ m = M ) -> [_ m / k ]_ A = B )
25	19 24	sylan2b	|- ( ( ( M e. V /\ B e. CC ) /\ m e. { M } ) -> [_ m / k ]_ A = B )
26		simplr	|- ( ( ( M e. V /\ B e. CC ) /\ m e. { M } ) -> B e. CC )
27	25 26	eqeltrd	|- ( ( ( M e. V /\ B e. CC ) /\ m e. { M } ) -> [_ m / k ]_ A e. CC )
28	13	eleq2i	|- ( n e. ( 1 ... 1 ) <-> n e. { 1 } )
29		velsn	|- ( n e. { 1 } <-> n = 1 )
30	28 29	bitri	|- ( n e. ( 1 ... 1 ) <-> n = 1 )
31		fvsng	|- ( ( 1 e. ZZ /\ M e. V ) -> ( { <. 1 , M >. } ` 1 ) = M )
32	10 31	mpan	|- ( M e. V -> ( { <. 1 , M >. } ` 1 ) = M )
33	32	adantr	|- ( ( M e. V /\ B e. CC ) -> ( { <. 1 , M >. } ` 1 ) = M )
34	33	csbeq1d	|- ( ( M e. V /\ B e. CC ) -> [_ ( { <. 1 , M >. } ` 1 ) / k ]_ A = [_ M / k ]_ A )
35		simpr	|- ( ( M e. V /\ B e. CC ) -> B e. CC )
36		fvsng	|- ( ( 1 e. ZZ /\ B e. CC ) -> ( { <. 1 , B >. } ` 1 ) = B )
37	10 35 36	sylancr	|- ( ( M e. V /\ B e. CC ) -> ( { <. 1 , B >. } ` 1 ) = B )
38	23 34 37	3eqtr4rd	|- ( ( M e. V /\ B e. CC ) -> ( { <. 1 , B >. } ` 1 ) = [_ ( { <. 1 , M >. } ` 1 ) / k ]_ A )
39		fveq2	|- ( n = 1 -> ( { <. 1 , B >. } ` n ) = ( { <. 1 , B >. } ` 1 ) )
40		fveq2	|- ( n = 1 -> ( { <. 1 , M >. } ` n ) = ( { <. 1 , M >. } ` 1 ) )
41	40	csbeq1d	|- ( n = 1 -> [_ ( { <. 1 , M >. } ` n ) / k ]_ A = [_ ( { <. 1 , M >. } ` 1 ) / k ]_ A )
42	39 41	eqeq12d	|- ( n = 1 -> ( ( { <. 1 , B >. } ` n ) = [_ ( { <. 1 , M >. } ` n ) / k ]_ A <-> ( { <. 1 , B >. } ` 1 ) = [_ ( { <. 1 , M >. } ` 1 ) / k ]_ A ) )
43	38 42	syl5ibrcom	|- ( ( M e. V /\ B e. CC ) -> ( n = 1 -> ( { <. 1 , B >. } ` n ) = [_ ( { <. 1 , M >. } ` n ) / k ]_ A ) )
44	43	imp	|- ( ( ( M e. V /\ B e. CC ) /\ n = 1 ) -> ( { <. 1 , B >. } ` n ) = [_ ( { <. 1 , M >. } ` n ) / k ]_ A )
45	30 44	sylan2b	|- ( ( ( M e. V /\ B e. CC ) /\ n e. ( 1 ... 1 ) ) -> ( { <. 1 , B >. } ` n ) = [_ ( { <. 1 , M >. } ` n ) / k ]_ A )
46	7 9 18 27 45	fprod	|- ( ( M e. V /\ B e. CC ) -> prod_ m e. { M } [_ m / k ]_ A = ( seq 1 ( x. , { <. 1 , B >. } ) ` 1 ) )
47	6 46	eqtrid	|- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = ( seq 1 ( x. , { <. 1 , B >. } ) ` 1 ) )
48	10 37	seq1i	|- ( ( M e. V /\ B e. CC ) -> ( seq 1 ( x. , { <. 1 , B >. } ) ` 1 ) = B )
49	47 48	eqtrd	|- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )