Step | Hyp | Ref
| Expression |
1 | | prod0 14512 |
. . . 4
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
2 | | fprodf1o.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐹:𝐶–1-1-onto→𝐴) |
4 | | f1oeq2 6041 |
. . . . . . . . 9
⊢ (𝐶 = ∅ → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:∅–1-1-onto→𝐴)) |
5 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 = ∅) → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:∅–1-1-onto→𝐴)) |
6 | 3, 5 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐹:∅–1-1-onto→𝐴) |
7 | | f1ofo 6057 |
. . . . . . 7
⊢ (𝐹:∅–1-1-onto→𝐴 → 𝐹:∅–onto→𝐴) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐹:∅–onto→𝐴) |
9 | | fo00 6084 |
. . . . . . 7
⊢ (𝐹:∅–onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) |
10 | 9 | simprbi 479 |
. . . . . 6
⊢ (𝐹:∅–onto→𝐴 → 𝐴 = ∅) |
11 | 8, 10 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐴 = ∅) |
12 | 11 | prodeq1d 14490 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
13 | | prodeq1 14478 |
. . . . . 6
⊢ (𝐶 = ∅ → ∏𝑛 ∈ 𝐶 𝐷 = ∏𝑛 ∈ ∅ 𝐷) |
14 | | prod0 14512 |
. . . . . 6
⊢
∏𝑛 ∈
∅ 𝐷 =
1 |
15 | 13, 14 | syl6eq 2660 |
. . . . 5
⊢ (𝐶 = ∅ → ∏𝑛 ∈ 𝐶 𝐷 = 1) |
16 | 15 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → ∏𝑛 ∈ 𝐶 𝐷 = 1) |
17 | 1, 12, 16 | 3eqtr4a 2670 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = ∅) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷) |
18 | 17 | ex 449 |
. 2
⊢ (𝜑 → (𝐶 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷)) |
19 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → (𝐹‘𝑚) = (𝐹‘(𝑓‘𝑛))) |
20 | 19 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
21 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (#‘𝐶) ∈
ℕ) |
22 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) |
23 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
24 | 2, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
25 | 24 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → (𝐹‘𝑚) ∈ 𝐴) |
26 | | fprodf1o.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
27 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
28 | 26, 27 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
29 | 28 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
30 | 25, 29 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
31 | 30 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
32 | | simpr 476 |
. . . . . . . . . . . 12
⊢
(((#‘𝐶) ∈
ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) → 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) |
33 | | f1oco 6072 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶–1-1-onto→𝐴 ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) → (𝐹 ∘ 𝑓):(1...(#‘𝐶))–1-1-onto→𝐴) |
34 | 2, 32, 33 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(#‘𝐶))–1-1-onto→𝐴) |
35 | | f1of 6050 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝑓):(1...(#‘𝐶))–1-1-onto→𝐴 → (𝐹 ∘ 𝑓):(1...(#‘𝐶))⟶𝐴) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(#‘𝐶))⟶𝐴) |
37 | | fvco3 6185 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝑓):(1...(#‘𝐶))⟶𝐴 ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
38 | 36, 37 | sylan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
39 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(#‘𝐶))–1-1-onto→𝐶 → 𝑓:(1...(#‘𝐶))⟶𝐶) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((#‘𝐶) ∈
ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) → 𝑓:(1...(#‘𝐶))⟶𝐶) |
41 | 40 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(#‘𝐶))⟶𝐶) |
42 | | fvco3 6185 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘𝐶))⟶𝐶 ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
43 | 41, 42 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
44 | 43 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
45 | 38, 44 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
46 | 20, 21, 22, 31, 45 | fprod 14510 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → ∏𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓)))‘(#‘𝐶))) |
47 | | fprodf1o.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
48 | 24 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
49 | 47, 48 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
50 | | fprodf1o.1 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
51 | 50, 27 | fvmpti 6190 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺) = ( I ‘𝐷)) |
52 | 49, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺) = ( I ‘𝐷)) |
53 | 47 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺)) |
54 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
55 | 54 | fvmpt2i 6199 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝐶 → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ( I ‘𝐷)) |
56 | 55 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ( I ‘𝐷)) |
57 | 52, 53, 56 | 3eqtr4rd 2655 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
58 | 57 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
59 | | nffvmpt1 6111 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) |
60 | 59 | nfeq1 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) |
61 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
62 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
64 | 61, 63 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) ↔ ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
65 | 60, 64 | rspc 3276 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝐶 → (∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
66 | 58, 65 | mpan9 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
67 | 66 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
68 | 67 | prodeq2dv 14492 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → ∏𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ∏𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
69 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = ((𝐹 ∘ 𝑓)‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
70 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
71 | 70 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
72 | 69, 21, 34, 71, 38 | fprod 14510 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓)))‘(#‘𝐶))) |
73 | 46, 68, 72 | 3eqtr4rd 2655 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
74 | | prodfc 14514 |
. . . . . 6
⊢
∏𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵 |
75 | | prodfc 14514 |
. . . . . 6
⊢
∏𝑚 ∈
𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ∏𝑛 ∈ 𝐶 𝐷 |
76 | 73, 74, 75 | 3eqtr3g 2667 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷) |
77 | 76 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝐶) ∈ ℕ) → (𝑓:(1...(#‘𝐶))–1-1-onto→𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷)) |
78 | 77 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘𝐶) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷)) |
79 | 78 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷)) |
80 | | fprodf1o.2 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
81 | | fz1f1o 14288 |
. . 3
⊢ (𝐶 ∈ Fin → (𝐶 = ∅ ∨ ((#‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶))) |
82 | 80, 81 | syl 17 |
. 2
⊢ (𝜑 → (𝐶 = ∅ ∨ ((#‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶))) |
83 | 18, 79, 82 | mpjaod 395 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷) |