Step | Hyp | Ref
| Expression |
1 | | prodeq1 14639 |
. . . 4
⊢ (𝑤 = ∅ → ∏𝑘 ∈ 𝑤 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
2 | 1 | mpteq2dv 4745 |
. . 3
⊢ (𝑤 = ∅ → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ ∅ 𝐶)) |
3 | 2 | eleq1d 2686 |
. 2
⊢ (𝑤 = ∅ → ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) ∈ (𝐴–cn→ℂ) ↔ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ ∅ 𝐶) ∈ (𝐴–cn→ℂ))) |
4 | | prodeq1 14639 |
. . . 4
⊢ (𝑤 = 𝑧 → ∏𝑘 ∈ 𝑤 𝐶 = ∏𝑘 ∈ 𝑧 𝐶) |
5 | 4 | mpteq2dv 4745 |
. . 3
⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶)) |
6 | 5 | eleq1d 2686 |
. 2
⊢ (𝑤 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) ∈ (𝐴–cn→ℂ) ↔ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ))) |
7 | | prodeq1 14639 |
. . . 4
⊢ (𝑤 = (𝑧 ∪ {𝑦}) → ∏𝑘 ∈ 𝑤 𝐶 = ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶) |
8 | 7 | mpteq2dv 4745 |
. . 3
⊢ (𝑤 = (𝑧 ∪ {𝑦}) → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶)) |
9 | 8 | eleq1d 2686 |
. 2
⊢ (𝑤 = (𝑧 ∪ {𝑦}) → ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) ∈ (𝐴–cn→ℂ) ↔ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶) ∈ (𝐴–cn→ℂ))) |
10 | | prodeq1 14639 |
. . . 4
⊢ (𝑤 = 𝐵 → ∏𝑘 ∈ 𝑤 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
11 | 10 | mpteq2dv 4745 |
. . 3
⊢ (𝑤 = 𝐵 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝐵 𝐶)) |
12 | 11 | eleq1d 2686 |
. 2
⊢ (𝑤 = 𝐵 → ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑤 𝐶) ∈ (𝐴–cn→ℂ) ↔ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝐵 𝐶) ∈ (𝐴–cn→ℂ))) |
13 | | prod0 14673 |
. . . . 5
⊢
∏𝑘 ∈
∅ 𝐶 =
1 |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ ∅ 𝐶 = 1) |
15 | 14 | mpteq2dv 4745 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ ∅ 𝐶) = (𝑥 ∈ 𝐴 ↦ 1)) |
16 | | fprodcncf.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
17 | | 1cnd 10056 |
. . . 4
⊢ (𝜑 → 1 ∈
ℂ) |
18 | | ssid 3624 |
. . . . 5
⊢ ℂ
⊆ ℂ |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
20 | 16, 17, 19 | constcncfg 40084 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 1) ∈ (𝐴–cn→ℂ)) |
21 | 15, 20 | eqeltrd 2701 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ ∅ 𝐶) ∈ (𝐴–cn→ℂ)) |
22 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑢∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶 |
23 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∪ {𝑦}) |
24 | | nfcsb1v 3549 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐶 |
25 | 23, 24 | nfcprod 14641 |
. . . . . 6
⊢
Ⅎ𝑥∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶 |
26 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝐶 = ⦋𝑢 / 𝑥⦌𝐶) |
27 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑘 ∈ (𝑧 ∪ {𝑦})) → 𝐶 = ⦋𝑢 / 𝑥⦌𝐶) |
28 | 27 | prodeq2dv 14653 |
. . . . . 6
⊢ (𝑥 = 𝑢 → ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶 = ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶) |
29 | 22, 25, 28 | cbvmpt 4749 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶) = (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶) |
30 | 29 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶) = (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶)) |
31 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) |
32 | | nfcsb1v 3549 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 |
33 | | fprodcncf.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ Fin) |
34 | 33 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → 𝐵 ∈ Fin) |
35 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → 𝑧 ⊆ 𝐵) |
36 | | ssfi 8180 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝑧 ⊆ 𝐵) → 𝑧 ∈ Fin) |
37 | 34, 35, 36 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → 𝑧 ∈ Fin) |
38 | 37 | adantrr 753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → 𝑧 ∈ Fin) |
39 | 38 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → 𝑧 ∈ Fin) |
40 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → 𝑦 ∈ V) |
42 | | eldifn 3733 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐵 ∖ 𝑧) → ¬ 𝑦 ∈ 𝑧) |
43 | 42 | ad2antll 765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → ¬ 𝑦 ∈ 𝑧) |
44 | 43 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → ¬ 𝑦 ∈ 𝑧) |
45 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) ∧ 𝑘 ∈ 𝑧) → 𝜑) |
46 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) ∧ 𝑘 ∈ 𝑧) → 𝑢 ∈ 𝐴) |
47 | 35 | adantrr 753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → 𝑧 ⊆ 𝐵) |
48 | 47 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) ∧ 𝑘 ∈ 𝑧) → 𝑧 ⊆ 𝐵) |
49 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) ∧ 𝑘 ∈ 𝑧) → 𝑘 ∈ 𝑧) |
50 | 48, 49 | sseldd 3604 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) ∧ 𝑘 ∈ 𝑧) → 𝑘 ∈ 𝐵) |
51 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) |
52 | 24 | nfel1 2779 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ |
53 | 51, 52 | nfim 1825 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
54 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴)) |
55 | 54 | 3anbi2d 1404 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
56 | 26 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐶 ∈ ℂ ↔ ⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ)) |
57 | 55, 56 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ))) |
58 | | fprodcncf.c |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
59 | 53, 57, 58 | chvar 2262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
60 | 45, 46, 50, 59 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) ∧ 𝑘 ∈ 𝑧) → ⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
61 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑘 = 𝑦 → ⦋𝑢 / 𝑥⦌𝐶 = ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) |
62 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → 𝜑) |
63 | | eldifi 3732 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐵 ∖ 𝑧) → 𝑦 ∈ 𝐵) |
64 | 63 | ad2antll 765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → 𝑦 ∈ 𝐵) |
65 | 64 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
66 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) |
67 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 ∈ 𝐴) → 𝜑) |
68 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) |
69 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
70 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
71 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘ℂ |
72 | 32, 71 | nfel 2777 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ |
73 | 70, 72 | nfim 1825 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
74 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
75 | 74 | 3anbi3d 1405 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
76 | 61 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → (⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ)) |
77 | 75, 76 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ))) |
78 | 73, 77, 59 | chvar 2262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
79 | 67, 68, 69, 78 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 ∈ 𝐴) → ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
80 | 62, 65, 66, 79 | syl21anc 1325 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶 ∈ ℂ) |
81 | 31, 32, 39, 41, 44, 60, 61, 80 | fprodsplitsn 14720 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ 𝑢 ∈ 𝐴) → ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶 = (∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶 · ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶)) |
82 | 81 | mpteq2dva 4744 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶) = (𝑢 ∈ 𝐴 ↦ (∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶 · ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶))) |
83 | 82 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶) = (𝑢 ∈ 𝐴 ↦ (∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶 · ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶))) |
84 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢∏𝑘 ∈ 𝑧 𝐶 |
85 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑧 |
86 | 85, 24 | nfcprod 14641 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶 |
87 | 26 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑘 ∈ 𝑧) → 𝐶 = ⦋𝑢 / 𝑥⦌𝐶) |
88 | 87 | prodeq2dv 14653 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → ∏𝑘 ∈ 𝑧 𝐶 = ∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶) |
89 | 84, 86, 88 | cbvmpt 4749 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) = (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶) |
90 | 89 | eqcomi 2631 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶) = (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) |
91 | 90 | a1i 11 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ) → (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶) = (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶)) |
92 | | id 22 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ) → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) |
93 | 91, 92 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ) → (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
94 | 93 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
95 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐵) |
96 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝐴 |
97 | 96, 32 | nfmpt 4746 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) |
98 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐴–cn→ℂ) |
99 | 97, 98 | nfel 2777 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ) |
100 | 95, 99 | nfim 1825 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
101 | 74 | anbi2d 740 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐵))) |
102 | 61 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑘 = 𝑦 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑥⦌𝐶 = ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) |
103 | 102 | mpteq2dva 4744 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑦 → (𝑢 ∈ 𝐴 ↦ ⦋𝑢 / 𝑥⦌𝐶) = (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶)) |
104 | 103 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → ((𝑢 ∈ 𝐴 ↦ ⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ) ↔ (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ))) |
105 | 101, 104 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑢 ∈ 𝐴 ↦ ⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)))) |
106 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢𝐶 |
107 | 106, 24, 26 | cbvmpt 4749 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑢 ∈ 𝐴 ↦ ⦋𝑢 / 𝑥⦌𝐶) |
108 | | fprodcncf.cn |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ (𝐴–cn→ℂ)) |
109 | 107, 108 | syl5eqelr 2706 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑢 ∈ 𝐴 ↦ ⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
110 | 100, 105,
109 | chvar 2262 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
111 | 64, 110 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
112 | 111 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑢 ∈ 𝐴 ↦ ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
113 | 94, 112 | mulcncf 23215 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑢 ∈ 𝐴 ↦ (∏𝑘 ∈ 𝑧 ⦋𝑢 / 𝑥⦌𝐶 · ⦋𝑦 / 𝑘⦌⦋𝑢 / 𝑥⦌𝐶)) ∈ (𝐴–cn→ℂ)) |
114 | 83, 113 | eqeltrd 2701 |
. . . 4
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑢 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})⦋𝑢 / 𝑥⦌𝐶) ∈ (𝐴–cn→ℂ)) |
115 | 30, 114 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) ∧ (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ)) → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶) ∈ (𝐴–cn→ℂ)) |
116 | 115 | ex 450 |
. 2
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐵 ∧ 𝑦 ∈ (𝐵 ∖ 𝑧))) → ((𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝑧 𝐶) ∈ (𝐴–cn→ℂ) → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ (𝑧 ∪ {𝑦})𝐶) ∈ (𝐴–cn→ℂ))) |
117 | 3, 6, 9, 12, 21, 116, 33 | findcard2d 8202 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝐵 𝐶) ∈ (𝐴–cn→ℂ)) |