Step | Hyp | Ref
| Expression |
1 | | fprodcl2lem.5 |
. . . 4
⊢ (𝜑 → 𝐴 ≠ ∅) |
2 | 1 | a1d 25 |
. . 3
⊢ (𝜑 → (¬ ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 → 𝐴 ≠ ∅)) |
3 | 2 | necon4bd 2802 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)) |
4 | | prodfc 14514 |
. . . . . . 7
⊢
∏𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵 |
5 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑥) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) |
6 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
ℕ) |
7 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) |
8 | | fprodcllem.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
9 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ ℂ) |
10 | | fprodcllem.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) |
11 | 9, 10 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
12 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
13 | 11, 12 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
14 | 13 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
15 | 14 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
16 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))⟶𝐴) |
17 | 16 | ad2antll 761 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))⟶𝐴) |
18 | | fvco3 6185 |
. . . . . . . . 9
⊢ ((𝑓:(1...(#‘𝐴))⟶𝐴 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) |
19 | 17, 18 | sylan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) |
20 | 5, 6, 7, 15, 19 | fprod 14510 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
21 | 4, 20 | syl5eqr 2658 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
22 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
23 | 6, 22 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
(ℤ≥‘1)) |
24 | 10, 12 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝑆) |
25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝑆) |
26 | | fco 5971 |
. . . . . . . . 9
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝑆 ∧ 𝑓:(1...(#‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(#‘𝐴))⟶𝑆) |
27 | 25, 17, 26 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(#‘𝐴))⟶𝑆) |
28 | 27 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥) ∈ 𝑆) |
29 | | fprodcllem.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
30 | 29 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
31 | 23, 28, 30 | seqcl 12683 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (seq1( · ,
((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴)) ∈ 𝑆) |
32 | 21, 31 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |
33 | 32 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝐴) ∈ ℕ) → (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)) |
34 | 33 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)) |
35 | 34 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)) |
36 | | fprodcllem.3 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
37 | | fz1f1o 14288 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
38 | 36, 37 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
39 | 3, 35, 38 | mpjaod 395 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |