Theorem prodsn 15312

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

Hypothesis

Ref	Expression
prodsn.1	⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)

Assertion

Ref	Expression
prodsn	⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵)

Distinct variable groups:   𝐵,𝑘   𝑘,𝑀   𝑘,𝑉

Allowed substitution hint:   𝐴(𝑘)

Proof of Theorem prodsn

Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2976	. . . 4 ⊢ Ⅎ𝑚𝐴
2		nfcsb1v 3904	. . . 4 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐴
3		csbeq1a 3894	. . . 4 ⊢ (𝑘 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑘⦌𝐴)
4	1, 2, 3	cbvprodi 15267	. . 3 ⊢ ∏𝑘 ∈ {𝑀}𝐴 = ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴
5		csbeq1 3883	. . . 4 ⊢ (𝑚 = ({⟨1, 𝑀⟩}‘𝑛) → ⦋𝑚 / 𝑘⦌𝐴 = ⦋({⟨1, 𝑀⟩}‘𝑛) / 𝑘⦌𝐴)
6		1nn 11646	. . . . 5 ⊢ 1 ∈ ℕ
7	6	a1i 11	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 1 ∈ ℕ)
8		1z 12010	. . . . . 6 ⊢ 1 ∈ ℤ
9		f1osng 6652	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ 𝑉) → {⟨1, 𝑀⟩}:{1}–1-1-onto→{𝑀})
10		fzsn 12947	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (1...1) = {1})
11	8, 10	ax-mp 5	. . . . . . . 8 ⊢ (1...1) = {1}
12		f1oeq2 6602	. . . . . . . 8 ⊢ ((1...1) = {1} → ({⟨1, 𝑀⟩}:(1...1)–1-1-onto→{𝑀} ↔ {⟨1, 𝑀⟩}:{1}–1-1-onto→{𝑀}))
13	11, 12	ax-mp 5	. . . . . . 7 ⊢ ({⟨1, 𝑀⟩}:(1...1)–1-1-onto→{𝑀} ↔ {⟨1, 𝑀⟩}:{1}–1-1-onto→{𝑀})
14	9, 13	sylibr 236	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ 𝑉) → {⟨1, 𝑀⟩}:(1...1)–1-1-onto→{𝑀})
15	8, 14	mpan 688	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → {⟨1, 𝑀⟩}:(1...1)–1-1-onto→{𝑀})
16	15	adantr 483	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → {⟨1, 𝑀⟩}:(1...1)–1-1-onto→{𝑀})
17		velsn 4580	. . . . . 6 ⊢ (𝑚 ∈ {𝑀} ↔ 𝑚 = 𝑀)
18		csbeq1 3883	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ⦋𝑚 / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴)
19		nfcvd 2977	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑘𝐵)
20		prodsn.1	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)
21	19, 20	csbiegf 3913	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵)
22	21	adantr 483	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵)
23	18, 22	sylan9eqr 2877	. . . . . 6 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 = 𝑀) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵)
24	17, 23	sylan2b 595	. . . . 5 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵)
25		simplr 767	. . . . 5 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → 𝐵 ∈ ℂ)
26	24, 25	eqeltrd 2912	. . . 4 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 ∈ ℂ)
27	11	eleq2i 2903	. . . . . 6 ⊢ (𝑛 ∈ (1...1) ↔ 𝑛 ∈ {1})
28		velsn 4580	. . . . . 6 ⊢ (𝑛 ∈ {1} ↔ 𝑛 = 1)
29	27, 28	bitri 277	. . . . 5 ⊢ (𝑛 ∈ (1...1) ↔ 𝑛 = 1)
30		fvsng 6939	. . . . . . . . . . 11 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ 𝑉) → ({⟨1, 𝑀⟩}‘1) = 𝑀)
31	8, 30	mpan 688	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → ({⟨1, 𝑀⟩}‘1) = 𝑀)
32	31	adantr 483	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({⟨1, 𝑀⟩}‘1) = 𝑀)
33	32	csbeq1d 3884	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ⦋({⟨1, 𝑀⟩}‘1) / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴)
34		simpr 487	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
35		fvsng 6939	. . . . . . . . 9 ⊢ ((1 ∈ ℤ ∧ 𝐵 ∈ ℂ) → ({⟨1, 𝐵⟩}‘1) = 𝐵)
36	8, 34, 35	sylancr 589	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({⟨1, 𝐵⟩}‘1) = 𝐵)
37	22, 33, 36	3eqtr4rd 2866	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({⟨1, 𝐵⟩}‘1) = ⦋({⟨1, 𝑀⟩}‘1) / 𝑘⦌𝐴)
38		fveq2 6667	. . . . . . . 8 ⊢ (𝑛 = 1 → ({⟨1, 𝐵⟩}‘𝑛) = ({⟨1, 𝐵⟩}‘1))
39		fveq2 6667	. . . . . . . . 9 ⊢ (𝑛 = 1 → ({⟨1, 𝑀⟩}‘𝑛) = ({⟨1, 𝑀⟩}‘1))
40	39	csbeq1d 3884	. . . . . . . 8 ⊢ (𝑛 = 1 → ⦋({⟨1, 𝑀⟩}‘𝑛) / 𝑘⦌𝐴 = ⦋({⟨1, 𝑀⟩}‘1) / 𝑘⦌𝐴)
41	38, 40	eqeq12d 2836	. . . . . . 7 ⊢ (𝑛 = 1 → (({⟨1, 𝐵⟩}‘𝑛) = ⦋({⟨1, 𝑀⟩}‘𝑛) / 𝑘⦌𝐴 ↔ ({⟨1, 𝐵⟩}‘1) = ⦋({⟨1, 𝑀⟩}‘1) / 𝑘⦌𝐴))
42	37, 41	syl5ibrcom 249	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (𝑛 = 1 → ({⟨1, 𝐵⟩}‘𝑛) = ⦋({⟨1, 𝑀⟩}‘𝑛) / 𝑘⦌𝐴))
43	42	imp 409	. . . . 5 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 = 1) → ({⟨1, 𝐵⟩}‘𝑛) = ⦋({⟨1, 𝑀⟩}‘𝑛) / 𝑘⦌𝐴)
44	29, 43	sylan2b 595	. . . 4 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (1...1)) → ({⟨1, 𝐵⟩}‘𝑛) = ⦋({⟨1, 𝑀⟩}‘𝑛) / 𝑘⦌𝐴)
45	5, 7, 16, 26, 44	fprod 15291	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 = (seq1( · , {⟨1, 𝐵⟩})‘1))
46	4, 45	syl5eq 2867	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = (seq1( · , {⟨1, 𝐵⟩})‘1))
47	8, 36	seq1i 13381	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (seq1( · , {⟨1, 𝐵⟩})‘1) = 𝐵)
48	46, 47	eqtrd 2855	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ⦋csb 3880  {csn 4564  ⟨cop 4570  –1-1-onto→wf1o 6351  ‘cfv 6352  (class class class)co 7153  ℂcc 10532  1c1 10535   · cmul 10539  ℕcn 11635  ℤcz 11979  ...cfz 12890  seqcseq 13367  ∏cprod 15255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5327  ax-un 7458  ax-inf2 9101  ax-cnex 10590  ax-resscn 10591  ax-1cn 10592  ax-icn 10593  ax-addcl 10594  ax-addrcl 10595  ax-mulcl 10596  ax-mulrcl 10597  ax-mulcom 10598  ax-addass 10599  ax-mulass 10600  ax-distr 10601  ax-i2m1 10602  ax-1ne0 10603  ax-1rid 10604  ax-rnegex 10605  ax-rrecex 10606  ax-cnre 10607  ax-pre-lttri 10608  ax-pre-lttrn 10609  ax-pre-ltadd 10610  ax-pre-mulgt0 10611  ax-pre-sup 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3495  df-sbc 3771  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4465  df-pw 4538  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4836  df-int 4874  df-iun 4918  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5457  df-eprel 5462  df-po 5471  df-so 5472  df-fr 5511  df-se 5512  df-we 5513  df-xp 5558  df-rel 5559  df-cnv 5560  df-co 5561  df-dm 5562  df-rn 5563  df-res 5564  df-ima 5565  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7111  df-ov 7156  df-oprab 7157  df-mpo 7158  df-om 7578  df-1st 7686  df-2nd 7687  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-1o 8099  df-oadd 8103  df-er 8286  df-en 8507  df-dom 8508  df-sdom 8509  df-fin 8510  df-sup 8903  df-oi 8971  df-card 9365  df-pnf 10674  df-mnf 10675  df-xr 10676  df-ltxr 10677  df-le 10678  df-sub 10869  df-neg 10870  df-div 11295  df-nn 11636  df-2 11698  df-3 11699  df-n0 11896  df-z 11980  df-uz 12242  df-rp 12388  df-fz 12891  df-fzo 13032  df-seq 13368  df-exp 13428  df-hash 13689  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-prod 15256

This theorem is referenced by:  fprod1  15313  fprodm1  15317  fprod1p  15318  prodsns  15322  fprod2dlem  15330  fprodefsum  15444  fprodfvdvdsd  15679  prmdvdsprmo  16374  fprodeq02  30539  prodpr  30542  prodtp  30543  prodfzo03  31898  hoidmv1le  42950  ovnovollem1  43012  ovnovollem2  43013  fmtnorec2  43779