Step | Hyp | Ref
| Expression |
1 | | 1t1e1 8985 |
. . . . 5
⊢ (1
· 1) = 1 |
2 | | prod0 11482 |
. . . . . 6
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
3 | | prod0 11482 |
. . . . . 6
⊢
∏𝑘 ∈
∅ 𝐶 =
1 |
4 | 2, 3 | oveq12i 5836 |
. . . . 5
⊢
(∏𝑘 ∈
∅ 𝐵 ·
∏𝑘 ∈ ∅
𝐶) = (1 ·
1) |
5 | | prod0 11482 |
. . . . 5
⊢
∏𝑘 ∈
∅ (𝐵 · 𝐶) = 1 |
6 | 1, 4, 5 | 3eqtr4ri 2189 |
. . . 4
⊢
∏𝑘 ∈
∅ (𝐵 · 𝐶) = (∏𝑘 ∈ ∅ 𝐵 · ∏𝑘 ∈ ∅ 𝐶) |
7 | | prodeq1 11450 |
. . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = ∏𝑘 ∈ ∅ (𝐵 · 𝐶)) |
8 | | prodeq1 11450 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
9 | | prodeq1 11450 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
10 | 8, 9 | oveq12d 5842 |
. . . 4
⊢ (𝐴 = ∅ → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶) = (∏𝑘 ∈ ∅ 𝐵 · ∏𝑘 ∈ ∅ 𝐶)) |
11 | 6, 7, 10 | 3eqtr4a 2216 |
. . 3
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)) |
12 | 11 | a1i 9 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))) |
13 | | simprl 521 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
ℕ) |
14 | | nnuz 9474 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
15 | 13, 14 | eleqtrdi 2250 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
(ℤ≥‘1)) |
16 | | elnnuz 9475 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℕ ↔ 𝑝 ∈
(ℤ≥‘1)) |
17 | 16 | biimpri 132 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘1) → 𝑝 ∈ ℕ) |
18 | 17 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ 𝑝 ∈
ℕ) |
19 | | fprodmul.2 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
20 | 19 | fmpttd 5622 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
21 | 20 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
22 | | f1of 5414 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
23 | 22 | ad2antll 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
24 | | fco 5335 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
25 | 21, 23, 24 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
26 | 25 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
27 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
𝑝 ≤ (♯‘𝐴)) |
28 | | simplr 520 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
𝑝 ∈
(ℤ≥‘1)) |
29 | 13 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(♯‘𝐴) ∈
ℕ) |
30 | 29 | nnzd 9285 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(♯‘𝐴) ∈
ℤ) |
31 | | elfz5 9920 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈
(ℤ≥‘1) ∧ (♯‘𝐴) ∈ ℤ) → (𝑝 ∈ (1...(♯‘𝐴)) ↔ 𝑝 ≤ (♯‘𝐴))) |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(𝑝 ∈
(1...(♯‘𝐴))
↔ 𝑝 ≤
(♯‘𝐴))) |
33 | 27, 32 | mpbird 166 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
𝑝 ∈
(1...(♯‘𝐴))) |
34 | 26, 33 | ffvelrnd 5603 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) ∈ ℂ) |
35 | | 1cnd 7894 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) → 1
∈ ℂ) |
36 | 18 | nnzd 9285 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ 𝑝 ∈
ℤ) |
37 | 13 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ (♯‘𝐴)
∈ ℕ) |
38 | 37 | nnzd 9285 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ (♯‘𝐴)
∈ ℤ) |
39 | | zdcle 9240 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → DECID 𝑝 ≤ (♯‘𝐴)) |
40 | 36, 38, 39 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ DECID 𝑝 ≤ (♯‘𝐴)) |
41 | 34, 35, 40 | ifcldadc 3534 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) |
42 | | breq1 3968 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑝 ≤ (♯‘𝐴))) |
43 | | fveq2 5468 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝)) |
44 | 42, 43 | ifbieq1d 3527 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1)) |
45 | | eqid 2157 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)) |
46 | 44, 45 | fvmptg 5544 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℕ ∧ if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1)) |
47 | 18, 41, 46 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1)) |
48 | 47, 41 | eqeltrd 2234 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) ∈ ℂ) |
49 | | fprodmul.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
50 | 49 | fmpttd 5622 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
51 | 50 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
52 | | fco 5335 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
53 | 51, 23, 52 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
54 | 53 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
55 | 54, 33 | ffvelrnd 5603 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝) ∈ ℂ) |
56 | 55, 35, 40 | ifcldadc 3534 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) |
57 | | fveq2 5468 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝)) |
58 | 42, 57 | ifbieq1d 3527 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) |
59 | | eqid 2157 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)) |
60 | 58, 59 | fvmptg 5544 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℕ ∧ if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) |
61 | 18, 56, 60 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) |
62 | 61, 56 | eqeltrd 2234 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝) ∈ ℂ) |
63 | 23 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
𝑓:(1...(♯‘𝐴))⟶𝐴) |
64 | 63, 33 | ffvelrnd 5603 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(𝑓‘𝑝) ∈ 𝐴) |
65 | | csbov12g 5860 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑝) ∈ 𝐴 → ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) = (⦋(𝑓‘𝑝) / 𝑘⦌𝐵 · ⦋(𝑓‘𝑝) / 𝑘⦌𝐶)) |
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) = (⦋(𝑓‘𝑝) / 𝑘⦌𝐵 · ⦋(𝑓‘𝑝) / 𝑘⦌𝐶)) |
67 | 19, 49 | mulcld 7898 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 · 𝐶) ∈ ℂ) |
68 | 67 | ralrimiva 2530 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ) |
69 | 68 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ) |
70 | | nfcsb1v 3064 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) |
71 | 70 | nfel1 2310 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ |
72 | | csbeq1a 3040 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑝) → (𝐵 · 𝐶) = ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶)) |
73 | 72 | eleq1d 2226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑝) → ((𝐵 · 𝐶) ∈ ℂ ↔
⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ)) |
74 | 71, 73 | rspc 2810 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝐵 · 𝐶) ∈ ℂ →
⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ)) |
75 | 64, 69, 74 | sylc 62 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ) |
76 | | eqid 2157 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) = (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) |
77 | 76 | fvmpts 5546 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘𝑝) ∈ 𝐴 ∧ ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶) ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶)) |
78 | 64, 75, 77 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌(𝐵 · 𝐶)) |
79 | 19 | ralrimiva 2530 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
80 | 79 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
81 | | nfcsb1v 3064 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐵 |
82 | 81 | nfel1 2310 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ |
83 | | csbeq1a 3040 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑓‘𝑝) → 𝐵 = ⦋(𝑓‘𝑝) / 𝑘⦌𝐵) |
84 | 83 | eleq1d 2226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑝) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ)) |
85 | 82, 84 | rspc 2810 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ)) |
86 | 64, 80, 85 | sylc 62 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ) |
87 | | eqid 2157 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
88 | 87 | fvmpts 5546 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑝) ∈ 𝐴 ∧ ⦋(𝑓‘𝑝) / 𝑘⦌𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐵) |
89 | 64, 86, 88 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐵) |
90 | 49 | ralrimiva 2530 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
91 | 90 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
92 | | nfcsb1v 3064 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐶 |
93 | 92 | nfel1 2310 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ |
94 | | csbeq1a 3040 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑓‘𝑝) → 𝐶 = ⦋(𝑓‘𝑝) / 𝑘⦌𝐶) |
95 | 94 | eleq1d 2226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑝) → (𝐶 ∈ ℂ ↔ ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ)) |
96 | 93, 95 | rspc 2810 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ → ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ)) |
97 | 64, 91, 96 | sylc 62 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ) |
98 | | eqid 2157 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶) |
99 | 98 | fvmpts 5546 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑝) ∈ 𝐴 ∧ ⦋(𝑓‘𝑝) / 𝑘⦌𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐶) |
100 | 64, 97, 99 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)) = ⦋(𝑓‘𝑝) / 𝑘⦌𝐶) |
101 | 89, 100 | oveq12d 5842 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) · ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝))) = (⦋(𝑓‘𝑝) / 𝑘⦌𝐵 · ⦋(𝑓‘𝑝) / 𝑘⦌𝐶)) |
102 | 66, 78, 101 | 3eqtr4d 2200 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) · ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)))) |
103 | | fvco3 5539 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑝 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝))) |
104 | 63, 33, 103 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝))) |
105 | | fvco3 5539 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑝 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝))) |
106 | 63, 33, 105 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝))) |
107 | | fvco3 5539 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑝 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝))) |
108 | 63, 33, 107 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝))) |
109 | 106, 108 | oveq12d 5842 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) · (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑝)) · ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑝)))) |
110 | 102, 104,
109 | 3eqtr4d 2200 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) · (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝))) |
111 | 27 | iftrued 3512 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝)) |
112 | 27 | iftrued 3512 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝)) |
113 | 27 | iftrued 3512 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝)) |
114 | 112, 113 | oveq12d 5842 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝) · (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝))) |
115 | 110, 111,
114 | 3eqtr4d 2200 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))) |
116 | 1 | eqcomi 2161 |
. . . . . . . . . . 11
⊢ 1 = (1
· 1) |
117 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) →
¬ 𝑝 ≤
(♯‘𝐴)) |
118 | 117 | iffalsed 3515 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = 1) |
119 | 117 | iffalsed 3515 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) = 1) |
120 | 117 | iffalsed 3515 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1) = 1) |
121 | 119, 120 | oveq12d 5842 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) →
(if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1)) = (1 · 1)) |
122 | 116, 118,
121 | 3eqtr4a 2216 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ ¬ 𝑝 ≤
(♯‘𝐴)) →
if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))) |
123 | | exmiddc 822 |
. . . . . . . . . . 11
⊢
(DECID 𝑝 ≤ (♯‘𝐴) → (𝑝 ≤ (♯‘𝐴) ∨ ¬ 𝑝 ≤ (♯‘𝐴))) |
124 | 40, 123 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ (𝑝 ≤
(♯‘𝐴) ∨
¬ 𝑝 ≤
(♯‘𝐴))) |
125 | 115, 122,
124 | mpjaodan 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))) |
126 | 78, 75 | eqeltrd 2234 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑝)) ∈ ℂ) |
127 | 104, 126 | eqeltrd 2234 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
∧ 𝑝 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝) ∈ ℂ) |
128 | 127, 35, 40 | ifcldadc 3534 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ if(𝑝 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) |
129 | | fveq2 5468 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝)) |
130 | 42, 129 | ifbieq1d 3527 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1)) |
131 | | eqid 2157 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)) |
132 | 130, 131 | fvmptg 5544 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℕ ∧ if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1)) |
133 | 18, 128, 132 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑝), 1)) |
134 | 47, 61 | oveq12d 5842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ (((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) · ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝)) = (if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑝), 1) · if(𝑝 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑝), 1))) |
135 | 125, 133,
134 | 3eqtr4d 2200 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1))‘𝑝) = (((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1))‘𝑝) · ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1))‘𝑝))) |
136 | 15, 48, 62, 135 | prod3fmul 11438 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)))) |
137 | | fveq2 5468 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑛))) |
138 | | simprr 522 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
139 | 67 | fmpttd 5622 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)):𝐴⟶ℂ) |
140 | 139 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)):𝐴⟶ℂ) |
141 | 140 | ffvelrnda 5602 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) ∈ ℂ) |
142 | | fvco3 5539 |
. . . . . . . . 9
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑛))) |
143 | 23, 142 | sylan 281 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘(𝑓‘𝑛))) |
144 | 137, 13, 138, 141, 143 | fprodseq 11480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴))) |
145 | | fveq2 5468 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
146 | 21 | ffvelrnda 5602 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
147 | | fvco3 5539 |
. . . . . . . . . 10
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
148 | 23, 147 | sylan 281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
149 | 145, 13, 138, 146, 148 | fprodseq 11480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴))) |
150 | | fveq2 5468 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
151 | 51 | ffvelrnda 5602 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ) |
152 | | fvco3 5539 |
. . . . . . . . . 10
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
153 | 23, 152 | sylan 281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
154 | 150, 13, 138, 151, 153 | fprodseq 11480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴))) |
155 | 149, 154 | oveq12d 5842 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 1)))‘(♯‘𝐴)))) |
156 | 136, 144,
155 | 3eqtr4d 2200 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚))) |
157 | | prodfct 11484 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 (𝐵 · 𝐶) ∈ ℂ → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶)) |
158 | 68, 157 | syl 14 |
. . . . . . 7
⊢ (𝜑 → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶)) |
159 | 158 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 · 𝐶))‘𝑚) = ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶)) |
160 | | prodfct 11484 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ ℂ → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵) |
161 | 79, 160 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵) |
162 | | prodfct 11484 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝐴 𝐶 ∈ ℂ → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶) |
163 | 90, 162 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶) |
164 | 161, 163 | oveq12d 5842 |
. . . . . . 7
⊢ (𝜑 → (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)) |
165 | 164 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) · ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)) |
166 | 156, 159,
165 | 3eqtr3d 2198 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)) |
167 | 166 | expr 373 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))) |
168 | 167 | exlimdv 1799 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))) |
169 | 168 | expimpd 361 |
. 2
⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))) |
170 | | fprodmul.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
171 | | fz1f1o 11272 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
172 | 170, 171 | syl 14 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
173 | 12, 169, 172 | mpjaod 708 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶)) |