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

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 ⊢ Ⅎ 𝑘 𝐵
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 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )