Metamath Proof Explorer


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 )