This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
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 eqtrid ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ( seq 1 ( · , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) )
47 9 36 seq1i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ( seq 1 ( · , { ⟨ 1 , 𝐵 ⟩ } ) ‘ 1 ) = 𝐵 )
48 46 47 eqtrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )