Metamath Proof Explorer

Theorem prodsn

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

Ref Expression
Hypothesis prodsn.1 
|- ( k = M -> A = B )
Assertion prodsn 
|- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )

Proof

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