fprodmul - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > fprodmul		GIF version

Theorem fprodmul 12175

Description: The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017.)

**Hypotheses**
Ref	Expression
fprodmul.1	⊢ (𝜑 → 𝐴 ∈ Fin)
fprodmul.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
fprodmul.3	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)

**Assertion**
Ref	Expression
fprodmul	⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))

Distinct variable groups: 𝐴,𝑘 𝜑,𝑘 Allowed substitution hints: 𝐵(𝑘) 𝐶(𝑘)

Proof of Theorem fprodmul Dummy variables 𝑝 𝑓 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1t1e1 9301	. . . . 5 ⊢ (1 · 1) = 1
2		prod0 12169	. . . . . 6 ⊢ ∏𝑘 ∈ ∅ 𝐵 = 1
3		prod0 12169	. . . . . 6 ⊢ ∏𝑘 ∈ ∅ 𝐶 = 1
4	2, 3	oveq12i 6035	. . . . 5 ⊢ (∏𝑘 ∈ ∅ 𝐵 · ∏𝑘 ∈ ∅ 𝐶) = (1 · 1)
5		prod0 12169	. . . . 5 ⊢ ∏𝑘 ∈ ∅ (𝐵 · 𝐶) = 1
6	1, 4, 5	3eqtr4ri 2262	. . . 4 ⊢ ∏𝑘 ∈ ∅ (𝐵 · 𝐶) = (∏𝑘 ∈ ∅ 𝐵 · ∏𝑘 ∈ ∅ 𝐶)
7		prodeq1 12137	. . . 4 ⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = ∏𝑘 ∈ ∅ (𝐵 · 𝐶))
8		prodeq1 12137	. . . . 5 ⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵)
9		prodeq1 12137	. . . . 5 ⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ ∅ 𝐶)
10	8, 9	oveq12d 6041	. . . 4 ⊢ (𝐴 = ∅ → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶) = (∏𝑘 ∈ ∅ 𝐵 · ∏𝑘 ∈ ∅ 𝐶))
11	6, 7, 10	3eqtr4a 2289	. . 3 ⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))
12	11	a1i 9	. 2 ⊢ (𝜑 → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)))
13		simprl 531	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ ℕ)
14		nnuz 9797	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
15	13, 14	eleqtrdi 2323	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘1))
16		elnnuz 9798	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℕ ↔ 𝑝 ∈ (ℤ_≥‘1))
17	16	biimpri 133	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (ℤ_≥‘1) → 𝑝 ∈ ℕ)
18	17	adantl 277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → 𝑝 ∈ ℕ)
19		fprodmul.2	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
20	19	fmpttd 5805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ)
21	20	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ)
22		f1of 5586	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴)
23	22	ad2antll 491	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
24		fco 5502	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
25	21, 23, 24	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
26	25	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
27		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑝 ≤ (♯‘𝐴))
28		simplr 529	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑝 ∈ (ℤ_≥‘1))
29	13	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (♯‘𝐴) ∈ ℕ)
30	29	nnzd 9606	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (♯‘𝐴) ∈ ℤ)
31		elfz5 10257	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ (ℤ_≥‘1) ∧ (♯‘𝐴) ∈ ℤ) → (𝑝 ∈ (1...(♯‘𝐴)) ↔ 𝑝 ≤ (♯‘𝐴)))
32	28, 30, 31	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (𝑝 ∈ (1...(♯‘𝐴)) ↔ 𝑝 ≤ (♯‘𝐴)))
33	27, 32	mpbird 167	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑝 ∈ (1...(♯‘𝐴)))
34	26, 33	ffvelcdmd 5786	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) ∈ ℂ)
35		1cnd 8200	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
36	18	nnzd 9606	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → 𝑝 ∈ ℤ)
37	13	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℕ)
38	37	nnzd 9606	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
39		zdcle 9561	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑝 ≤ (♯‘𝐴))
40	36, 38, 39	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → DECID 𝑝 ≤ (♯‘𝐴))
41	34, 35, 40	ifcldadc 3636	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) ∈ ℂ)
42		breq1 4092	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑝 ≤ (♯‘𝐴)))
43		fveq2 5642	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝))
44	42, 43	ifbieq1d 3629	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1))
45		eqid 2230	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))
46	44, 45	fvmptg 5725	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℕ ∧ if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1))
47	18, 41, 46	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1))
48	47, 41	eqeltrd 2307	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) ∈ ℂ)
49		fprodmul.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
50	49	fmpttd 5805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
51	50	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
52		fco 5502	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
53	51, 23, 52	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
54	53	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
55	54, 33	ffvelcdmd 5786	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝) ∈ ℂ)
56	55, 35, 40	ifcldadc 3636	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) ∈ ℂ)
57		fveq2 5642	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝))
58	42, 57	ifbieq1d 3629	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))
59		eqid 2230	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))
60	58, 59	fvmptg 5725	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℕ ∧ if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))
61	18, 56, 60	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))
62	61, 56	eqeltrd 2307	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝) ∈ ℂ)
63	23	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
64	63, 33	ffvelcdmd 5786	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (𝑓‘𝑝) ∈ 𝐴)
65		csbov12g 6063	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑝) ∈ 𝐴 → ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) = (⦋(𝑓‘𝑝) / 𝑘⦌𝐵 · ⦋(𝑓‘𝑝) / 𝑘⦌𝐶))
66	64, 65	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) = (⦋(𝑓‘𝑝) / 𝑘⦌𝐵 · ⦋(𝑓‘𝑝) / 𝑘⦌𝐶))
67	19, 49	mulcld 8205	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 · 𝐶) ∈ ℂ)
68	67	ralrimiva 2604	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ)
69	68	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ)
70		nfcsb1v 3159	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶)
71	70	nfel1 2384	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ
72		csbeq1a 3135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑝) → (𝐵 · 𝐶) = ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶))
73	72	eleq1d 2299	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑓‘𝑝) → ((𝐵 · 𝐶) ∈ ℂ ↔ ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ))
74	71, 73	rspc 2903	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ → ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ))
75	64, 69, 74	sylc 62	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ)
76		eqid 2230	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) = (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))
77	76	fvmpts 5727	. . . . . . . . . . . . . 14 ⊢ (((𝑓‘𝑝) ∈ 𝐴 ∧ ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶))
78	64, 75, 77	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶))
79	19	ralrimiva 2604	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
80	79	ad3antrrr 492	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
81		nfcsb1v 3159	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐵
82	81	nfel1 2384	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ
83		csbeq1a 3135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑓‘𝑝) → 𝐵 = ⦋(𝑓‘𝑝) / 𝑘⦌𝐵)
84	83	eleq1d 2299	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑝) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ))
85	82, 84	rspc 2903	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ))
86	64, 80, 85	sylc 62	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ)
87		eqid 2230	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
88	87	fvmpts 5727	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑝) ∈ 𝐴 ∧ ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐵)
89	64, 86, 88	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐵)
90	49	ralrimiva 2604	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
91	90	ad3antrrr 492	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
92		nfcsb1v 3159	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐶
93	92	nfel1 2384	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ
94		csbeq1a 3135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑓‘𝑝) → 𝐶 = ⦋(𝑓‘𝑝) / 𝑘⦌𝐶)
95	94	eleq1d 2299	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑝) → (𝐶 ∈ ℂ ↔ ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ))
96	93, 95	rspc 2903	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ → ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ))
97	64, 91, 96	sylc 62	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ)
98		eqid 2230	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶)
99	98	fvmpts 5727	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑝) ∈ 𝐴 ∧ ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐶)
100	64, 97, 99	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐶)
101	89, 100	oveq12d 6041	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) · ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝))) = (⦋(𝑓‘𝑝) / 𝑘⦌𝐵 · ⦋(𝑓‘𝑝) / 𝑘⦌𝐶))
102	66, 78, 101	3eqtr4d 2273	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) · ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝))))
103		fvco3 5720	. . . . . . . . . . . . 13 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑝 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)))
104	63, 33, 103	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)))
105		fvco3 5720	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑝 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)))
106	63, 33, 105	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)))
107		fvco3 5720	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑝 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)))
108	63, 33, 107	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)))
109	106, 108	oveq12d 6041	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) · (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) · ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝))))
110	102, 104, 109	3eqtr4d 2273	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) · (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝)))
111	27	iftrued 3613	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝))
112	27	iftrued 3613	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝))
113	27	iftrued 3613	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝))
114	112, 113	oveq12d 6041	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) · (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝)))
115	110, 111, 114	3eqtr4d 2273	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)))
116	1	eqcomi 2234	. . . . . . . . . . 11 ⊢ 1 = (1 · 1)
117		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → ¬ 𝑝 ≤ (♯‘𝐴))
118	117	iffalsed 3616	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = 1)
119	117	iffalsed 3616	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) = 1)
120	117	iffalsed 3616	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) = 1)
121	119, 120	oveq12d 6041	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) = (1 · 1))
122	116, 118, 121	3eqtr4a 2289	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)))
123		exmiddc 843	. . . . . . . . . . 11 ⊢ (DECID 𝑝 ≤ (♯‘𝐴) → (𝑝 ≤ (♯‘𝐴) ∨ ¬ 𝑝 ≤ (♯‘𝐴)))
124	40, 123	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → (𝑝 ≤ (♯‘𝐴) ∨ ¬ 𝑝 ≤ (♯‘𝐴)))
125	115, 122, 124	mpjaodan 805	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)))
126	78, 75	eqeltrd 2307	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) ∈ ℂ)
127	104, 126	eqeltrd 2307	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) ∧ 𝑝 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) ∈ ℂ)
128	127, 35, 40	ifcldadc 3636	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) ∈ ℂ)
129		fveq2 5642	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝))
130	42, 129	ifbieq1d 3629	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1))
131		eqid 2230	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))
132	130, 131	fvmptg 5725	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℕ ∧ if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1))
133	18, 128, 132	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1))
134	47, 61	oveq12d 6041	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → (((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) · ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝)) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)))
135	125, 133, 134	3eqtr4d 2273	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))‘𝑝) = (((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) · ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝)))
136	15, 48, 62, 135	prod3fmul 12125	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴))))
137		fveq2 5642	. . . . . . . 8 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑛)))
138		simprr 533	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
139	67	fmpttd 5805	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)):𝐴⟶ℂ)
140	139	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)):𝐴⟶ℂ)
141	140	ffvelcdmda 5785	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) ∈ ℂ)
142		fvco3 5720	. . . . . . . . 9 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑛)))
143	23, 142	sylan 283	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑛)))
144	137, 13, 138, 141, 143	fprodseq 12167	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)))
145		fveq2 5642	. . . . . . . . 9 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
146	21	ffvelcdmda 5785	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ)
147		fvco3 5720	. . . . . . . . . 10 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
148	23, 147	sylan 283	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
149	145, 13, 138, 146, 148	fprodseq 12167	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)))
150		fveq2 5642	. . . . . . . . 9 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
151	51	ffvelcdmda 5785	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ)
152		fvco3 5720	. . . . . . . . . 10 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
153	23, 152	sylan 283	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
154	150, 13, 138, 151, 153	fprodseq 12167	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)))
155	149, 154	oveq12d 6041	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴))))
156	136, 144, 155	3eqtr4d 2273	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)))
157		prodfct 12171	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶))
158	68, 157	syl 14	. . . . . . 7 ⊢ (𝜑 → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶))
159	158	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶))
160		prodfct 12171	. . . . . . . . 9 ⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵)
161	79, 160	syl 14	. . . . . . . 8 ⊢ (𝜑 → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵)
162		prodfct 12171	. . . . . . . . 9 ⊢ (∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶)
163	90, 162	syl 14	. . . . . . . 8 ⊢ (𝜑 → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶)
164	161, 163	oveq12d 6041	. . . . . . 7 ⊢ (𝜑 → (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))
165	164	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))
166	156, 159, 165	3eqtr3d 2271	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))
167	166	expr 375	. . . 4 ⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)))
168	167	exlimdv 1866	. . 3 ⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)))
169	168	expimpd 363	. 2 ⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)))
170		fprodmul.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
171		fz1f1o 11958	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
172	170, 171	syl 14	. 2 ⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
173	12, 169, 172	mpjaod 725	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 715 DECID wdc 841 = wceq 1397 ∃wex 1540 ∈ wcel 2201 ∀wral 2509 ⦋csb 3126 ∅c0 3493 ifcif 3604 class class class wbr 4089 ↦ cmpt 4151 ∘ ccom 4731 ⟶wf 5324 –1-1-onto→wf1o 5327 ‘cfv 5328 (class class class)co 6023 Fincfn 6914 ℂcc 8035 1c1 8038 · cmul 8042 ≤ cle 8220 ℕcn 9148 ℤcz 9484 ℤ_≥cuz 9760 ...cfz 10248 seqcseq 10715 ♯chash 11043 ∏cprod 12134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-coll 4205 ax-sep 4208 ax-nul 4216 ax-pow 4266 ax-pr 4301 ax-un 4532 ax-setind 4637 ax-iinf 4688 ax-cnex 8128 ax-resscn 8129 ax-1cn 8130 ax-1re 8131 ax-icn 8132 ax-addcl 8133 ax-addrcl 8134 ax-mulcl 8135 ax-mulrcl 8136 ax-addcom 8137 ax-mulcom 8138 ax-addass 8139 ax-mulass 8140 ax-distr 8141 ax-i2m1 8142 ax-0lt1 8143 ax-1rid 8144 ax-0id 8145 ax-rnegex 8146 ax-precex 8147 ax-cnre 8148 ax-pre-ltirr 8149 ax-pre-ltwlin 8150 ax-pre-lttrn 8151 ax-pre-apti 8152 ax-pre-ltadd 8153 ax-pre-mulgt0 8154 ax-pre-mulext 8155 ax-arch 8156 ax-caucvg 8157

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rmo 2517 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-nul 3494 df-if 3605 df-pw 3655 df-sn 3676 df-pr 3677 df-op 3679 df-uni 3895 df-int 3930 df-iun 3973 df-br 4090 df-opab 4152 df-mpt 4153 df-tr 4189 df-id 4392 df-po 4395 df-iso 4396 df-iord 4465 df-on 4467 df-ilim 4468 df-suc 4470 df-iom 4691 df-xp 4733 df-rel 4734 df-cnv 4735 df-co 4736 df-dm 4737 df-rn 4738 df-res 4739 df-ima 4740 df-iota 5288 df-fun 5330 df-fn 5331 df-f 5332 df-f1 5333 df-fo 5334 df-f1o 5335 df-fv 5336 df-isom 5337 df-riota 5976 df-ov 6026 df-oprab 6027 df-mpo 6028 df-1st 6308 df-2nd 6309 df-recs 6476 df-irdg 6541 df-frec 6562 df-1o 6587 df-oadd 6591 df-er 6707 df-en 6915 df-dom 6916 df-fin 6917 df-pnf 8221 df-mnf 8222 df-xr 8223 df-ltxr 8224 df-le 8225 df-sub 8357 df-neg 8358 df-reap 8760 df-ap 8767 df-div 8858 df-inn 9149 df-2 9207 df-3 9208 df-4 9209 df-n0 9408 df-z 9485 df-uz 9761 df-q 9859 df-rp 9894 df-fz 10249 df-fzo 10383 df-seqfrec 10716 df-exp 10807 df-ihash 11044 df-cj 11425 df-re 11426 df-im 11427 df-rsqrt 11581 df-abs 11582 df-clim 11862 df-proddc 12135

This theorem is referenced by: fprodsplitdc 12180 fproddivap 12214 gausslemma2dlem5 15824 gausslemma2dlem6 15825

W3C validator