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

Theorem fprodcom2 15332
 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 5537 . . . . . . . . 9 Rel ({𝑗} × 𝐵)
21rgenw 3118 . . . . . . . 8 𝑗𝐴 Rel ({𝑗} × 𝐵)
3 reliun 5653 . . . . . . . 8 (Rel 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐵))
42, 3mpbir 234 . . . . . . 7 Rel 𝑗𝐴 ({𝑗} × 𝐵)
5 relcnv 5934 . . . . . . 7 Rel 𝑘𝐶 ({𝑘} × 𝐷)
6 ancom 464 . . . . . . . . . . . 12 ((𝑥 = 𝑗𝑦 = 𝑘) ↔ (𝑦 = 𝑘𝑥 = 𝑗))
7 vex 3444 . . . . . . . . . . . . 13 𝑥 ∈ V
8 vex 3444 . . . . . . . . . . . . 13 𝑦 ∈ V
97, 8opth 5333 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ (𝑥 = 𝑗𝑦 = 𝑘))
108, 7opth 5333 . . . . . . . . . . . 12 (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ↔ (𝑦 = 𝑘𝑥 = 𝑗))
116, 9, 103bitr4i 306 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩)
1211a1i 11 . . . . . . . . . 10 (𝜑 → (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩))
13 fprodcom2.4 . . . . . . . . . 10 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
1412, 13anbi12d 633 . . . . . . . . 9 (𝜑 → ((⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
15142exbidv 1925 . . . . . . . 8 (𝜑 → (∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
16 eliunxp 5672 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)))
177, 8opelcnv 5716 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
18 eliunxp 5672 . . . . . . . . 9 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
19 excom 2166 . . . . . . . . 9 (∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2017, 18, 193bitri 300 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2115, 16, 203bitr4g 317 . . . . . . 7 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷)))
224, 5, 21eqrelrdv 5629 . . . . . 6 (𝜑 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
23 nfcv 2955 . . . . . . 7 𝑥({𝑗} × 𝐵)
24 nfcv 2955 . . . . . . . 8 𝑗{𝑥}
25 nfcsb1v 3852 . . . . . . . 8 𝑗𝑥 / 𝑗𝐵
2624, 25nfxp 5552 . . . . . . 7 𝑗({𝑥} × 𝑥 / 𝑗𝐵)
27 sneq 4535 . . . . . . . 8 (𝑗 = 𝑥 → {𝑗} = {𝑥})
28 csbeq1a 3842 . . . . . . . 8 (𝑗 = 𝑥𝐵 = 𝑥 / 𝑗𝐵)
2927, 28xpeq12d 5550 . . . . . . 7 (𝑗 = 𝑥 → ({𝑗} × 𝐵) = ({𝑥} × 𝑥 / 𝑗𝐵))
3023, 26, 29cbviun 4923 . . . . . 6 𝑗𝐴 ({𝑗} × 𝐵) = 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)
31 nfcv 2955 . . . . . . . 8 𝑦({𝑘} × 𝐷)
32 nfcv 2955 . . . . . . . . 9 𝑘{𝑦}
33 nfcsb1v 3852 . . . . . . . . 9 𝑘𝑦 / 𝑘𝐷
3432, 33nfxp 5552 . . . . . . . 8 𝑘({𝑦} × 𝑦 / 𝑘𝐷)
35 sneq 4535 . . . . . . . . 9 (𝑘 = 𝑦 → {𝑘} = {𝑦})
36 csbeq1a 3842 . . . . . . . . 9 (𝑘 = 𝑦𝐷 = 𝑦 / 𝑘𝐷)
3735, 36xpeq12d 5550 . . . . . . . 8 (𝑘 = 𝑦 → ({𝑘} × 𝐷) = ({𝑦} × 𝑦 / 𝑘𝐷))
3831, 34, 37cbviun 4923 . . . . . . 7 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
3938cnveqi 5709 . . . . . 6 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
4022, 30, 393eqtr3g 2856 . . . . 5 (𝜑 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
4140prodeq1d 15269 . . . 4 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
428, 7op1std 7683 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) = 𝑦)
4342csbeq1d 3832 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸)
448, 7op2ndd 7684 . . . . . . . 8 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) = 𝑥)
4544csbeq1d 3832 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
4645csbeq2dv 3835 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
4743, 46eqtrd 2833 . . . . 5 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
487, 8op2ndd 7684 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
4948csbeq1d 3832 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸)
507, 8op1std 7683 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5150csbeq1d 3832 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
5251csbeq2dv 3835 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
5349, 52eqtrd 2833 . . . . 5 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
54 fprodcom2.2 . . . . . 6 (𝜑𝐶 ∈ Fin)
55 snfi 8579 . . . . . . . 8 {𝑦} ∈ Fin
56 fprodcom2.1 . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
5756adantr 484 . . . . . . . . 9 ((𝜑𝑦𝐶) → 𝐴 ∈ Fin)
5833, 36opeliunxp2f 7861 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ (𝑦𝐶𝑥𝑦 / 𝑘𝐷))
5917, 58sylbbr 239 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝑦 / 𝑘𝐷) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
6059adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
6122adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
6260, 61eleqtrrd 2893 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵))
63 eliun 4885 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
6462, 63sylib 221 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
65 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
66 opelxp 5555 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) ↔ (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
6765, 66sylib 221 . . . . . . . . . . . . . . . 16 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
6867simpld 498 . . . . . . . . . . . . . . 15 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ {𝑗})
69 elsni 4542 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → 𝑥 = 𝑗)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 = 𝑗)
71 simpl 486 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑗𝐴)
7270, 71eqeltrd 2890 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥𝐴)
7372rexlimiva 3240 . . . . . . . . . . . 12 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑥𝐴)
7464, 73syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑥𝐴)
7574expr 460 . . . . . . . . . 10 ((𝜑𝑦𝐶) → (𝑥𝑦 / 𝑘𝐷𝑥𝐴))
7675ssrdv 3921 . . . . . . . . 9 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷𝐴)
7757, 76ssfid 8727 . . . . . . . 8 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷 ∈ Fin)
78 xpfi 8775 . . . . . . . 8 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑘𝐷 ∈ Fin) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
7955, 77, 78sylancr 590 . . . . . . 7 ((𝜑𝑦𝐶) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
8079ralrimiva 3149 . . . . . 6 (𝜑 → ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
81 iunfi 8798 . . . . . 6 ((𝐶 ∈ Fin ∧ ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin) → 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
8254, 80, 81syl2anc 587 . . . . 5 (𝜑 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
83 reliun 5653 . . . . . . 7 (Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∀𝑦𝐶 Rel ({𝑦} × 𝑦 / 𝑘𝐷))
84 relxp 5537 . . . . . . . 8 Rel ({𝑦} × 𝑦 / 𝑘𝐷)
8584a1i 11 . . . . . . 7 (𝑦𝐶 → Rel ({𝑦} × 𝑦 / 𝑘𝐷))
8683, 85mprgbir 3121 . . . . . 6 Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
8786a1i 11 . . . . 5 (𝜑 → Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
88 csbeq1 3831 . . . . . . . 8 (𝑥 = (2nd𝑤) → 𝑥 / 𝑗𝐸 = (2nd𝑤) / 𝑗𝐸)
8988csbeq2dv 3835 . . . . . . 7 (𝑥 = (2nd𝑤) → (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
9089eleq1d 2874 . . . . . 6 (𝑥 = (2nd𝑤) → ((1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ))
91 csbeq1 3831 . . . . . . . 8 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝐷 = (1st𝑤) / 𝑘𝐷)
92 csbeq1 3831 . . . . . . . . 9 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘𝑥 / 𝑗𝐸)
9392eleq1d 2874 . . . . . . . 8 (𝑦 = (1st𝑤) → (𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
9491, 93raleqbidv 3354 . . . . . . 7 (𝑦 = (1st𝑤) → (∀𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
95 simpl 486 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝜑)
9625nfcri 2943 . . . . . . . . . . . 12 𝑗 𝑦𝑥 / 𝑗𝐵
9769equcomd 2026 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑗} → 𝑗 = 𝑥)
9897, 28syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑗} → 𝐵 = 𝑥 / 𝑗𝐵)
9998eleq2d 2875 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → (𝑦𝐵𝑦𝑥 / 𝑗𝐵))
10099biimpa 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ {𝑗} ∧ 𝑦𝐵) → 𝑦𝑥 / 𝑗𝐵)
10166, 100sylbi 220 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
102101a1i 11 . . . . . . . . . . . 12 (𝑗𝐴 → (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵))
10396, 102rexlimi 3274 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
10464, 103syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦𝑥 / 𝑗𝐵)
105 fprodcom2.5 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
106105ralrimivva 3156 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ)
107 nfcsb1v 3852 . . . . . . . . . . . . . . . 16 𝑗𝑥 / 𝑗𝐸
108107nfel1 2971 . . . . . . . . . . . . . . 15 𝑗𝑥 / 𝑗𝐸 ∈ ℂ
10925, 108nfralw 3189 . . . . . . . . . . . . . 14 𝑗𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ
110 csbeq1a 3842 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑥𝐸 = 𝑥 / 𝑗𝐸)
111110eleq1d 2874 . . . . . . . . . . . . . . 15 (𝑗 = 𝑥 → (𝐸 ∈ ℂ ↔ 𝑥 / 𝑗𝐸 ∈ ℂ))
11228, 111raleqbidv 3354 . . . . . . . . . . . . . 14 (𝑗 = 𝑥 → (∀𝑘𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
113109, 112rspc 3559 . . . . . . . . . . . . 13 (𝑥𝐴 → (∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
114106, 113mpan9 510 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ)
115 nfcsb1v 3852 . . . . . . . . . . . . . 14 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸
116115nfel1 2971 . . . . . . . . . . . . 13 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ
117 csbeq1a 3842 . . . . . . . . . . . . . 14 (𝑘 = 𝑦𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
118117eleq1d 2874 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (𝑥 / 𝑗𝐸 ∈ ℂ ↔ 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
119116, 118rspc 3559 . . . . . . . . . . . 12 (𝑦𝑥 / 𝑗𝐵 → (∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
120114, 119syl5com 31 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑦𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
121120impr 458 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝑥 / 𝑗𝐵)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
12295, 74, 104, 121syl12anc 835 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
123122ralrimivva 3156 . . . . . . . 8 (𝜑 → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
124123adantr 484 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
125 simpr 488 . . . . . . . . 9 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
126 eliun 4885 . . . . . . . . 9 (𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
127125, 126sylib 221 . . . . . . . 8 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
128 xp1st 7705 . . . . . . . . . . . 12 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ {𝑦})
129128adantl 485 . . . . . . . . . . 11 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ {𝑦})
130 elsni 4542 . . . . . . . . . . 11 ((1st𝑤) ∈ {𝑦} → (1st𝑤) = 𝑦)
131129, 130syl 17 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) = 𝑦)
132 simpl 486 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶)
133131, 132eqeltrd 2890 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
134133rexlimiva 3240 . . . . . . . 8 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ 𝐶)
135127, 134syl 17 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
13694, 124, 135rspcdva 3573 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
137 xp2nd 7706 . . . . . . . . . 10 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
138137adantl 485 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
139131csbeq1d 3832 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘𝐷 = 𝑦 / 𝑘𝐷)
140138, 139eleqtrrd 2893 . . . . . . . 8 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
141140rexlimiva 3240 . . . . . . 7 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
142127, 141syl 17 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
14390, 136, 142rspcdva 3573 . . . . 5 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ)
14447, 53, 82, 87, 143fprodcnv 15331 . . . 4 (𝜑 → ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
14541, 144eqtr4d 2836 . . 3 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
146 fprodcom2.3 . . . . . 6 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
147146ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
14825nfel1 2971 . . . . . 6 𝑗𝑥 / 𝑗𝐵 ∈ Fin
14928eleq1d 2874 . . . . . 6 (𝑗 = 𝑥 → (𝐵 ∈ Fin ↔ 𝑥 / 𝑗𝐵 ∈ Fin))
150148, 149rspc 3559 . . . . 5 (𝑥𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑥 / 𝑗𝐵 ∈ Fin))
151147, 150mpan9 510 . . . 4 ((𝜑𝑥𝐴) → 𝑥 / 𝑗𝐵 ∈ Fin)
15253, 56, 151, 121fprod2d 15329 . . 3 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
15347, 54, 77, 122fprod2d 15329 . . 3 (𝜑 → ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
154145, 152, 1533eqtr4d 2843 . 2 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
155 nfcv 2955 . . 3 𝑥𝑘𝐵 𝐸
156 nfcv 2955 . . . . 5 𝑗𝑦
157156, 107nfcsbw 3854 . . . 4 𝑗𝑦 / 𝑘𝑥 / 𝑗𝐸
15825, 157nfcprod 15259 . . 3 𝑗𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
159 nfcv 2955 . . . . 5 𝑦𝐸
160 nfcsb1v 3852 . . . . 5 𝑘𝑦 / 𝑘𝐸
161 csbeq1a 3842 . . . . 5 (𝑘 = 𝑦𝐸 = 𝑦 / 𝑘𝐸)
162159, 160, 161cbvprodi 15265 . . . 4 𝑘𝐵 𝐸 = ∏𝑦𝐵 𝑦 / 𝑘𝐸
163110csbeq2dv 3835 . . . . . 6 (𝑗 = 𝑥𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
164163adantr 484 . . . . 5 ((𝑗 = 𝑥𝑦𝐵) → 𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
16528, 164prodeq12dv 15274 . . . 4 (𝑗 = 𝑥 → ∏𝑦𝐵 𝑦 / 𝑘𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
166162, 165syl5eq 2845 . . 3 (𝑗 = 𝑥 → ∏𝑘𝐵 𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
167155, 158, 166cbvprodi 15265 . 2 𝑗𝐴𝑘𝐵 𝐸 = ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
168 nfcv 2955 . . 3 𝑦𝑗𝐷 𝐸
16933, 115nfcprod 15259 . . 3 𝑘𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
170 nfcv 2955 . . . . 5 𝑥𝐸
171170, 107, 110cbvprodi 15265 . . . 4 𝑗𝐷 𝐸 = ∏𝑥𝐷 𝑥 / 𝑗𝐸
172117adantr 484 . . . . 5 ((𝑘 = 𝑦𝑥𝐷) → 𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17336, 172prodeq12dv 15274 . . . 4 (𝑘 = 𝑦 → ∏𝑥𝐷 𝑥 / 𝑗𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
174171, 173syl5eq 2845 . . 3 (𝑘 = 𝑦 → ∏𝑗𝐷 𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
175168, 169, 174cbvprodi 15265 . 2 𝑘𝐶𝑗𝐷 𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
176154, 167, 1753eqtr4g 2858 1 (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  ⦋csb 3828  {csn 4525  ⟨cop 4531  ∪ ciun 4881   × cxp 5517  ◡ccnv 5518  Rel wrel 5524  ‘cfv 6324  1st c1st 7671  2nd c2nd 7672  Fincfn 8494  ℂcc 10526  ∏cprod 15253 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-sup 8892  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-n0 11888  df-z 11972  df-uz 12234  df-rp 12380  df-fz 12888  df-fzo 13031  df-seq 13367  df-exp 13428  df-hash 13689  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-prod 15254 This theorem is referenced by:  fprodcom  15333  fprod0diag  15334
 Copyright terms: Public domain W3C validator