MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fprodcom2 Structured version   Visualization version   GIF version

Theorem fprodcom2 15546
Description: Interchange order of multiplication. Note that 𝐵(𝑗) and 𝐷(𝑘) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
Hypotheses
Ref Expression
fprodcom2.1 (𝜑𝐴 ∈ Fin)
fprodcom2.2 (𝜑𝐶 ∈ Fin)
fprodcom2.3 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
fprodcom2.4 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
fprodcom2.5 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
Assertion
Ref Expression
fprodcom2 (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑘   𝐶,𝑗,𝑘   𝐷,𝑗   𝜑,𝑗,𝑘
Allowed substitution hints:   𝐵(𝑗)   𝐷(𝑘)   𝐸(𝑗,𝑘)

Proof of Theorem fprodcom2
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 5569 . . . . . . . . 9 Rel ({𝑗} × 𝐵)
21rgenw 3073 . . . . . . . 8 𝑗𝐴 Rel ({𝑗} × 𝐵)
3 reliun 5686 . . . . . . . 8 (Rel 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐵))
42, 3mpbir 234 . . . . . . 7 Rel 𝑗𝐴 ({𝑗} × 𝐵)
5 relcnv 5972 . . . . . . 7 Rel 𝑘𝐶 ({𝑘} × 𝐷)
6 ancom 464 . . . . . . . . . . . 12 ((𝑥 = 𝑗𝑦 = 𝑘) ↔ (𝑦 = 𝑘𝑥 = 𝑗))
7 vex 3412 . . . . . . . . . . . . 13 𝑥 ∈ V
8 vex 3412 . . . . . . . . . . . . 13 𝑦 ∈ V
97, 8opth 5360 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ (𝑥 = 𝑗𝑦 = 𝑘))
108, 7opth 5360 . . . . . . . . . . . 12 (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ↔ (𝑦 = 𝑘𝑥 = 𝑗))
116, 9, 103bitr4i 306 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩)
1211a1i 11 . . . . . . . . . 10 (𝜑 → (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩))
13 fprodcom2.4 . . . . . . . . . 10 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
1412, 13anbi12d 634 . . . . . . . . 9 (𝜑 → ((⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
15142exbidv 1932 . . . . . . . 8 (𝜑 → (∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
16 eliunxp 5706 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)))
177, 8opelcnv 5750 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
18 eliunxp 5706 . . . . . . . . 9 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
19 excom 2166 . . . . . . . . 9 (∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2017, 18, 193bitri 300 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2115, 16, 203bitr4g 317 . . . . . . 7 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷)))
224, 5, 21eqrelrdv 5662 . . . . . 6 (𝜑 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
23 nfcv 2904 . . . . . . 7 𝑥({𝑗} × 𝐵)
24 nfcv 2904 . . . . . . . 8 𝑗{𝑥}
25 nfcsb1v 3836 . . . . . . . 8 𝑗𝑥 / 𝑗𝐵
2624, 25nfxp 5584 . . . . . . 7 𝑗({𝑥} × 𝑥 / 𝑗𝐵)
27 sneq 4551 . . . . . . . 8 (𝑗 = 𝑥 → {𝑗} = {𝑥})
28 csbeq1a 3825 . . . . . . . 8 (𝑗 = 𝑥𝐵 = 𝑥 / 𝑗𝐵)
2927, 28xpeq12d 5582 . . . . . . 7 (𝑗 = 𝑥 → ({𝑗} × 𝐵) = ({𝑥} × 𝑥 / 𝑗𝐵))
3023, 26, 29cbviun 4945 . . . . . 6 𝑗𝐴 ({𝑗} × 𝐵) = 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)
31 nfcv 2904 . . . . . . . 8 𝑦({𝑘} × 𝐷)
32 nfcv 2904 . . . . . . . . 9 𝑘{𝑦}
33 nfcsb1v 3836 . . . . . . . . 9 𝑘𝑦 / 𝑘𝐷
3432, 33nfxp 5584 . . . . . . . 8 𝑘({𝑦} × 𝑦 / 𝑘𝐷)
35 sneq 4551 . . . . . . . . 9 (𝑘 = 𝑦 → {𝑘} = {𝑦})
36 csbeq1a 3825 . . . . . . . . 9 (𝑘 = 𝑦𝐷 = 𝑦 / 𝑘𝐷)
3735, 36xpeq12d 5582 . . . . . . . 8 (𝑘 = 𝑦 → ({𝑘} × 𝐷) = ({𝑦} × 𝑦 / 𝑘𝐷))
3831, 34, 37cbviun 4945 . . . . . . 7 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
3938cnveqi 5743 . . . . . 6 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
4022, 30, 393eqtr3g 2801 . . . . 5 (𝜑 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
4140prodeq1d 15483 . . . 4 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
428, 7op1std 7771 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) = 𝑦)
4342csbeq1d 3815 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸)
448, 7op2ndd 7772 . . . . . . . 8 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) = 𝑥)
4544csbeq1d 3815 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
4645csbeq2dv 3818 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
4743, 46eqtrd 2777 . . . . 5 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
487, 8op2ndd 7772 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
4948csbeq1d 3815 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸)
507, 8op1std 7771 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5150csbeq1d 3815 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
5251csbeq2dv 3818 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
5349, 52eqtrd 2777 . . . . 5 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
54 fprodcom2.2 . . . . . 6 (𝜑𝐶 ∈ Fin)
55 snfi 8721 . . . . . . . 8 {𝑦} ∈ Fin
56 fprodcom2.1 . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
5756adantr 484 . . . . . . . . 9 ((𝜑𝑦𝐶) → 𝐴 ∈ Fin)
5833, 36opeliunxp2f 7952 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ (𝑦𝐶𝑥𝑦 / 𝑘𝐷))
5917, 58sylbbr 239 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝑦 / 𝑘𝐷) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
6059adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
6122adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
6260, 61eleqtrrd 2841 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵))
63 eliun 4908 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
6462, 63sylib 221 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
65 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
66 opelxp 5587 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) ↔ (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
6765, 66sylib 221 . . . . . . . . . . . . . . . 16 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
6867simpld 498 . . . . . . . . . . . . . . 15 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ {𝑗})
69 elsni 4558 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → 𝑥 = 𝑗)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 = 𝑗)
71 simpl 486 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑗𝐴)
7270, 71eqeltrd 2838 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥𝐴)
7372rexlimiva 3200 . . . . . . . . . . . 12 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑥𝐴)
7464, 73syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑥𝐴)
7574expr 460 . . . . . . . . . 10 ((𝜑𝑦𝐶) → (𝑥𝑦 / 𝑘𝐷𝑥𝐴))
7675ssrdv 3907 . . . . . . . . 9 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷𝐴)
7757, 76ssfid 8898 . . . . . . . 8 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷 ∈ Fin)
78 xpfi 8942 . . . . . . . 8 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑘𝐷 ∈ Fin) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
7955, 77, 78sylancr 590 . . . . . . 7 ((𝜑𝑦𝐶) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
8079ralrimiva 3105 . . . . . 6 (𝜑 → ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
81 iunfi 8964 . . . . . 6 ((𝐶 ∈ Fin ∧ ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin) → 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
8254, 80, 81syl2anc 587 . . . . 5 (𝜑 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
83 reliun 5686 . . . . . . 7 (Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∀𝑦𝐶 Rel ({𝑦} × 𝑦 / 𝑘𝐷))
84 relxp 5569 . . . . . . . 8 Rel ({𝑦} × 𝑦 / 𝑘𝐷)
8584a1i 11 . . . . . . 7 (𝑦𝐶 → Rel ({𝑦} × 𝑦 / 𝑘𝐷))
8683, 85mprgbir 3076 . . . . . 6 Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
8786a1i 11 . . . . 5 (𝜑 → Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
88 csbeq1 3814 . . . . . . . 8 (𝑥 = (2nd𝑤) → 𝑥 / 𝑗𝐸 = (2nd𝑤) / 𝑗𝐸)
8988csbeq2dv 3818 . . . . . . 7 (𝑥 = (2nd𝑤) → (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
9089eleq1d 2822 . . . . . 6 (𝑥 = (2nd𝑤) → ((1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ))
91 csbeq1 3814 . . . . . . . 8 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝐷 = (1st𝑤) / 𝑘𝐷)
92 csbeq1 3814 . . . . . . . . 9 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘𝑥 / 𝑗𝐸)
9392eleq1d 2822 . . . . . . . 8 (𝑦 = (1st𝑤) → (𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
9491, 93raleqbidv 3313 . . . . . . 7 (𝑦 = (1st𝑤) → (∀𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
95 simpl 486 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝜑)
9625nfcri 2891 . . . . . . . . . . . 12 𝑗 𝑦𝑥 / 𝑗𝐵
9769equcomd 2027 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑗} → 𝑗 = 𝑥)
9897, 28syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑗} → 𝐵 = 𝑥 / 𝑗𝐵)
9998eleq2d 2823 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → (𝑦𝐵𝑦𝑥 / 𝑗𝐵))
10099biimpa 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ {𝑗} ∧ 𝑦𝐵) → 𝑦𝑥 / 𝑗𝐵)
10166, 100sylbi 220 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
102101a1i 11 . . . . . . . . . . . 12 (𝑗𝐴 → (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵))
10396, 102rexlimi 3234 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
10464, 103syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦𝑥 / 𝑗𝐵)
105 fprodcom2.5 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
106105ralrimivva 3112 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ)
107 nfcsb1v 3836 . . . . . . . . . . . . . . . 16 𝑗𝑥 / 𝑗𝐸
108107nfel1 2920 . . . . . . . . . . . . . . 15 𝑗𝑥 / 𝑗𝐸 ∈ ℂ
10925, 108nfralw 3147 . . . . . . . . . . . . . 14 𝑗𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ
110 csbeq1a 3825 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑥𝐸 = 𝑥 / 𝑗𝐸)
111110eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑗 = 𝑥 → (𝐸 ∈ ℂ ↔ 𝑥 / 𝑗𝐸 ∈ ℂ))
11228, 111raleqbidv 3313 . . . . . . . . . . . . . 14 (𝑗 = 𝑥 → (∀𝑘𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
113109, 112rspc 3525 . . . . . . . . . . . . 13 (𝑥𝐴 → (∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
114106, 113mpan9 510 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ)
115 nfcsb1v 3836 . . . . . . . . . . . . . 14 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸
116115nfel1 2920 . . . . . . . . . . . . 13 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ
117 csbeq1a 3825 . . . . . . . . . . . . . 14 (𝑘 = 𝑦𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
118117eleq1d 2822 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (𝑥 / 𝑗𝐸 ∈ ℂ ↔ 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
119116, 118rspc 3525 . . . . . . . . . . . 12 (𝑦𝑥 / 𝑗𝐵 → (∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
120114, 119syl5com 31 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑦𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
121120impr 458 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝑥 / 𝑗𝐵)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
12295, 74, 104, 121syl12anc 837 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
123122ralrimivva 3112 . . . . . . . 8 (𝜑 → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
124123adantr 484 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
125 simpr 488 . . . . . . . . 9 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
126 eliun 4908 . . . . . . . . 9 (𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
127125, 126sylib 221 . . . . . . . 8 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
128 xp1st 7793 . . . . . . . . . . . 12 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ {𝑦})
129128adantl 485 . . . . . . . . . . 11 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ {𝑦})
130 elsni 4558 . . . . . . . . . . 11 ((1st𝑤) ∈ {𝑦} → (1st𝑤) = 𝑦)
131129, 130syl 17 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) = 𝑦)
132 simpl 486 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶)
133131, 132eqeltrd 2838 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
134133rexlimiva 3200 . . . . . . . 8 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ 𝐶)
135127, 134syl 17 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
13694, 124, 135rspcdva 3539 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
137 xp2nd 7794 . . . . . . . . . 10 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
138137adantl 485 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
139131csbeq1d 3815 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘𝐷 = 𝑦 / 𝑘𝐷)
140138, 139eleqtrrd 2841 . . . . . . . 8 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
141140rexlimiva 3200 . . . . . . 7 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
142127, 141syl 17 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
14390, 136, 142rspcdva 3539 . . . . 5 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ)
14447, 53, 82, 87, 143fprodcnv 15545 . . . 4 (𝜑 → ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
14541, 144eqtr4d 2780 . . 3 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
146 fprodcom2.3 . . . . . 6 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
147146ralrimiva 3105 . . . . 5 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
14825nfel1 2920 . . . . . 6 𝑗𝑥 / 𝑗𝐵 ∈ Fin
14928eleq1d 2822 . . . . . 6 (𝑗 = 𝑥 → (𝐵 ∈ Fin ↔ 𝑥 / 𝑗𝐵 ∈ Fin))
150148, 149rspc 3525 . . . . 5 (𝑥𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑥 / 𝑗𝐵 ∈ Fin))
151147, 150mpan9 510 . . . 4 ((𝜑𝑥𝐴) → 𝑥 / 𝑗𝐵 ∈ Fin)
15253, 56, 151, 121fprod2d 15543 . . 3 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
15347, 54, 77, 122fprod2d 15543 . . 3 (𝜑 → ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
154145, 152, 1533eqtr4d 2787 . 2 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
155 nfcv 2904 . . 3 𝑥𝑘𝐵 𝐸
156 nfcv 2904 . . . . 5 𝑗𝑦
157156, 107nfcsbw 3838 . . . 4 𝑗𝑦 / 𝑘𝑥 / 𝑗𝐸
15825, 157nfcprod 15473 . . 3 𝑗𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
159 nfcv 2904 . . . . 5 𝑦𝐸
160 nfcsb1v 3836 . . . . 5 𝑘𝑦 / 𝑘𝐸
161 csbeq1a 3825 . . . . 5 (𝑘 = 𝑦𝐸 = 𝑦 / 𝑘𝐸)
162159, 160, 161cbvprodi 15479 . . . 4 𝑘𝐵 𝐸 = ∏𝑦𝐵 𝑦 / 𝑘𝐸
163110csbeq2dv 3818 . . . . . 6 (𝑗 = 𝑥𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
164163adantr 484 . . . . 5 ((𝑗 = 𝑥𝑦𝐵) → 𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
16528, 164prodeq12dv 15488 . . . 4 (𝑗 = 𝑥 → ∏𝑦𝐵 𝑦 / 𝑘𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
166162, 165syl5eq 2790 . . 3 (𝑗 = 𝑥 → ∏𝑘𝐵 𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
167155, 158, 166cbvprodi 15479 . 2 𝑗𝐴𝑘𝐵 𝐸 = ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
168 nfcv 2904 . . 3 𝑦𝑗𝐷 𝐸
16933, 115nfcprod 15473 . . 3 𝑘𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
170 nfcv 2904 . . . . 5 𝑥𝐸
171170, 107, 110cbvprodi 15479 . . . 4 𝑗𝐷 𝐸 = ∏𝑥𝐷 𝑥 / 𝑗𝐸
172117adantr 484 . . . . 5 ((𝑘 = 𝑦𝑥𝐷) → 𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17336, 172prodeq12dv 15488 . . . 4 (𝑘 = 𝑦 → ∏𝑥𝐷 𝑥 / 𝑗𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
174171, 173syl5eq 2790 . . 3 (𝑘 = 𝑦 → ∏𝑗𝐷 𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
175168, 169, 174cbvprodi 15479 . 2 𝑘𝐶𝑗𝐷 𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
176154, 167, 1753eqtr4g 2803 1 (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wex 1787  wcel 2110  wral 3061  wrex 3062  csb 3811  {csn 4541  cop 4547   ciun 4904   × cxp 5549  ccnv 5550  Rel wrel 5556  cfv 6380  1st c1st 7759  2nd c2nd 7760  Fincfn 8626  cc 10727  cprod 15467
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-oi 9126  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-rp 12587  df-fz 13096  df-fzo 13239  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-prod 15468
This theorem is referenced by:  fprodcom  15547  fprod0diag  15548
  Copyright terms: Public domain W3C validator