ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fprodcom2fi GIF version

Theorem fprodcom2fi 11647
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)
fprodcom2fi.d ((𝜑𝑘𝐶) → 𝐷 ∈ Fin)
fprodcom2.4 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
fprodcom2.5 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
Assertion
Ref Expression
fprodcom2fi (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑘   𝐶,𝑗,𝑘   𝐷,𝑗   𝜑,𝑗,𝑘
Allowed substitution hints:   𝐵(𝑗)   𝐷(𝑘)   𝐸(𝑗,𝑘)

Proof of Theorem fprodcom2fi
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 4747 . . . . . . . . 9 Rel ({𝑗} × 𝐵)
21rgenw 2542 . . . . . . . 8 𝑗𝐴 Rel ({𝑗} × 𝐵)
3 reliun 4759 . . . . . . . 8 (Rel 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐵))
42, 3mpbir 146 . . . . . . 7 Rel 𝑗𝐴 ({𝑗} × 𝐵)
5 relcnv 5018 . . . . . . 7 Rel 𝑘𝐶 ({𝑘} × 𝐷)
6 ancom 266 . . . . . . . . . . . 12 ((𝑥 = 𝑗𝑦 = 𝑘) ↔ (𝑦 = 𝑘𝑥 = 𝑗))
7 vex 2752 . . . . . . . . . . . . 13 𝑥 ∈ V
8 vex 2752 . . . . . . . . . . . . 13 𝑦 ∈ V
97, 8opth 4249 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ (𝑥 = 𝑗𝑦 = 𝑘))
108, 7opth 4249 . . . . . . . . . . . 12 (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ↔ (𝑦 = 𝑘𝑥 = 𝑗))
116, 9, 103bitr4i 212 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩)
1211a1i 9 . . . . . . . . . 10 (𝜑 → (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩))
13 fprodcom2.4 . . . . . . . . . 10 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
1412, 13anbi12d 473 . . . . . . . . 9 (𝜑 → ((⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
15142exbidv 1878 . . . . . . . 8 (𝜑 → (∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
16 eliunxp 4778 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)))
177, 8opelcnv 4821 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
18 eliunxp 4778 . . . . . . . . 9 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
19 excom 1674 . . . . . . . . 9 (∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2017, 18, 193bitri 206 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2115, 16, 203bitr4g 223 . . . . . . 7 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷)))
224, 5, 21eqrelrdv 4734 . . . . . 6 (𝜑 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
23 nfcv 2329 . . . . . . 7 𝑥({𝑗} × 𝐵)
24 nfcv 2329 . . . . . . . 8 𝑗{𝑥}
25 nfcsb1v 3102 . . . . . . . 8 𝑗𝑥 / 𝑗𝐵
2624, 25nfxp 4665 . . . . . . 7 𝑗({𝑥} × 𝑥 / 𝑗𝐵)
27 sneq 3615 . . . . . . . 8 (𝑗 = 𝑥 → {𝑗} = {𝑥})
28 csbeq1a 3078 . . . . . . . 8 (𝑗 = 𝑥𝐵 = 𝑥 / 𝑗𝐵)
2927, 28xpeq12d 4663 . . . . . . 7 (𝑗 = 𝑥 → ({𝑗} × 𝐵) = ({𝑥} × 𝑥 / 𝑗𝐵))
3023, 26, 29cbviun 3935 . . . . . 6 𝑗𝐴 ({𝑗} × 𝐵) = 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)
31 nfcv 2329 . . . . . . . 8 𝑦({𝑘} × 𝐷)
32 nfcv 2329 . . . . . . . . 9 𝑘{𝑦}
33 nfcsb1v 3102 . . . . . . . . 9 𝑘𝑦 / 𝑘𝐷
3432, 33nfxp 4665 . . . . . . . 8 𝑘({𝑦} × 𝑦 / 𝑘𝐷)
35 sneq 3615 . . . . . . . . 9 (𝑘 = 𝑦 → {𝑘} = {𝑦})
36 csbeq1a 3078 . . . . . . . . 9 (𝑘 = 𝑦𝐷 = 𝑦 / 𝑘𝐷)
3735, 36xpeq12d 4663 . . . . . . . 8 (𝑘 = 𝑦 → ({𝑘} × 𝐷) = ({𝑦} × 𝑦 / 𝑘𝐷))
3831, 34, 37cbviun 3935 . . . . . . 7 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
3938cnveqi 4814 . . . . . 6 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
4022, 30, 393eqtr3g 2243 . . . . 5 (𝜑 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
4140prodeq1d 11585 . . . 4 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
428, 7op1std 6162 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) = 𝑦)
4342csbeq1d 3076 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸)
448, 7op2ndd 6163 . . . . . . . 8 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) = 𝑥)
4544csbeq1d 3076 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
4645csbeq2dv 3095 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
4743, 46eqtrd 2220 . . . . 5 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
487, 8op2ndd 6163 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
4948csbeq1d 3076 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸)
507, 8op1std 6162 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5150csbeq1d 3076 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
5251csbeq2dv 3095 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
5349, 52eqtrd 2220 . . . . 5 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
54 fprodcom2.2 . . . . . 6 (𝜑𝐶 ∈ Fin)
55 snfig 6827 . . . . . . . . 9 (𝑦 ∈ V → {𝑦} ∈ Fin)
5655elv 2753 . . . . . . . 8 {𝑦} ∈ Fin
57 fprodcom2fi.d . . . . . . . . . 10 ((𝜑𝑘𝐶) → 𝐷 ∈ Fin)
5857ralrimiva 2560 . . . . . . . . 9 (𝜑 → ∀𝑘𝐶 𝐷 ∈ Fin)
5933nfel1 2340 . . . . . . . . . 10 𝑘𝑦 / 𝑘𝐷 ∈ Fin
6036eleq1d 2256 . . . . . . . . . 10 (𝑘 = 𝑦 → (𝐷 ∈ Fin ↔ 𝑦 / 𝑘𝐷 ∈ Fin))
6159, 60rspc 2847 . . . . . . . . 9 (𝑦𝐶 → (∀𝑘𝐶 𝐷 ∈ Fin → 𝑦 / 𝑘𝐷 ∈ Fin))
6258, 61mpan9 281 . . . . . . . 8 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷 ∈ Fin)
63 xpfi 6942 . . . . . . . 8 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑘𝐷 ∈ Fin) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6456, 62, 63sylancr 414 . . . . . . 7 ((𝜑𝑦𝐶) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6564ralrimiva 2560 . . . . . 6 (𝜑 → ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
66 disjsnxp 6251 . . . . . . 7 Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
6766a1i 9 . . . . . 6 (𝜑Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
68 iunfidisj 6958 . . . . . 6 ((𝐶 ∈ Fin ∧ ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin ∧ Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6954, 65, 67, 68syl3anc 1248 . . . . 5 (𝜑 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
70 reliun 4759 . . . . . . 7 (Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∀𝑦𝐶 Rel ({𝑦} × 𝑦 / 𝑘𝐷))
71 relxp 4747 . . . . . . . 8 Rel ({𝑦} × 𝑦 / 𝑘𝐷)
7271a1i 9 . . . . . . 7 (𝑦𝐶 → Rel ({𝑦} × 𝑦 / 𝑘𝐷))
7370, 72mprgbir 2545 . . . . . 6 Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
7473a1i 9 . . . . 5 (𝜑 → Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
75 csbeq1 3072 . . . . . . . 8 (𝑥 = (2nd𝑤) → 𝑥 / 𝑗𝐸 = (2nd𝑤) / 𝑗𝐸)
7675csbeq2dv 3095 . . . . . . 7 (𝑥 = (2nd𝑤) → (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
7776eleq1d 2256 . . . . . 6 (𝑥 = (2nd𝑤) → ((1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ))
78 csbeq1 3072 . . . . . . . 8 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝐷 = (1st𝑤) / 𝑘𝐷)
79 csbeq1 3072 . . . . . . . . 9 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘𝑥 / 𝑗𝐸)
8079eleq1d 2256 . . . . . . . 8 (𝑦 = (1st𝑤) → (𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
8178, 80raleqbidv 2695 . . . . . . 7 (𝑦 = (1st𝑤) → (∀𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
82 simpl 109 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝜑)
8333, 36opeliunxp2f 6252 . . . . . . . . . . . . . . 15 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ (𝑦𝐶𝑥𝑦 / 𝑘𝐷))
8417, 83sylbbr 136 . . . . . . . . . . . . . 14 ((𝑦𝐶𝑥𝑦 / 𝑘𝐷) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
8584adantl 277 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
8622adantr 276 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
8785, 86eleqtrrd 2267 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵))
88 eliun 3902 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
8987, 88sylib 122 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
90 simpr 110 . . . . . . . . . . . . . . . 16 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
91 opelxp 4668 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) ↔ (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
9290, 91sylib 122 . . . . . . . . . . . . . . 15 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
9392simpld 112 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ {𝑗})
94 elsni 3622 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑗} → 𝑥 = 𝑗)
9593, 94syl 14 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 = 𝑗)
96 simpl 109 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑗𝐴)
9795, 96eqeltrd 2264 . . . . . . . . . . . 12 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥𝐴)
9897rexlimiva 2599 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑥𝐴)
9989, 98syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑥𝐴)
10025nfcri 2323 . . . . . . . . . . . 12 𝑗 𝑦𝑥 / 𝑗𝐵
10194equcomd 1717 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑗} → 𝑗 = 𝑥)
102101, 28syl 14 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑗} → 𝐵 = 𝑥 / 𝑗𝐵)
103102eleq2d 2257 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → (𝑦𝐵𝑦𝑥 / 𝑗𝐵))
104103biimpa 296 . . . . . . . . . . . . . 14 ((𝑥 ∈ {𝑗} ∧ 𝑦𝐵) → 𝑦𝑥 / 𝑗𝐵)
10591, 104sylbi 121 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
106105a1i 9 . . . . . . . . . . . 12 (𝑗𝐴 → (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵))
107100, 106rexlimi 2597 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
10889, 107syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦𝑥 / 𝑗𝐵)
109 fprodcom2.5 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
110109ralrimivva 2569 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ)
111 nfcsb1v 3102 . . . . . . . . . . . . . . . 16 𝑗𝑥 / 𝑗𝐸
112111nfel1 2340 . . . . . . . . . . . . . . 15 𝑗𝑥 / 𝑗𝐸 ∈ ℂ
11325, 112nfralw 2524 . . . . . . . . . . . . . 14 𝑗𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ
114 csbeq1a 3078 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑥𝐸 = 𝑥 / 𝑗𝐸)
115114eleq1d 2256 . . . . . . . . . . . . . . 15 (𝑗 = 𝑥 → (𝐸 ∈ ℂ ↔ 𝑥 / 𝑗𝐸 ∈ ℂ))
11628, 115raleqbidv 2695 . . . . . . . . . . . . . 14 (𝑗 = 𝑥 → (∀𝑘𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
117113, 116rspc 2847 . . . . . . . . . . . . 13 (𝑥𝐴 → (∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
118110, 117mpan9 281 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ)
119 nfcsb1v 3102 . . . . . . . . . . . . . 14 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸
120119nfel1 2340 . . . . . . . . . . . . 13 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ
121 csbeq1a 3078 . . . . . . . . . . . . . 14 (𝑘 = 𝑦𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
122121eleq1d 2256 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (𝑥 / 𝑗𝐸 ∈ ℂ ↔ 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
123120, 122rspc 2847 . . . . . . . . . . . 12 (𝑦𝑥 / 𝑗𝐵 → (∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
124118, 123syl5com 29 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑦𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
125124impr 379 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝑥 / 𝑗𝐵)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
12682, 99, 108, 125syl12anc 1246 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
127126ralrimivva 2569 . . . . . . . 8 (𝜑 → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
128127adantr 276 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
129 simpr 110 . . . . . . . . 9 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
130 eliun 3902 . . . . . . . . 9 (𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
131129, 130sylib 122 . . . . . . . 8 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
132 xp1st 6179 . . . . . . . . . . . 12 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ {𝑦})
133132adantl 277 . . . . . . . . . . 11 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ {𝑦})
134 elsni 3622 . . . . . . . . . . 11 ((1st𝑤) ∈ {𝑦} → (1st𝑤) = 𝑦)
135133, 134syl 14 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) = 𝑦)
136 simpl 109 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶)
137135, 136eqeltrd 2264 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
138137rexlimiva 2599 . . . . . . . 8 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ 𝐶)
139131, 138syl 14 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
14081, 128, 139rspcdva 2858 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
141 xp2nd 6180 . . . . . . . . . 10 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
142141adantl 277 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
143135csbeq1d 3076 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘𝐷 = 𝑦 / 𝑘𝐷)
144142, 143eleqtrrd 2267 . . . . . . . 8 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
145144rexlimiva 2599 . . . . . . 7 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
146131, 145syl 14 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
14777, 140, 146rspcdva 2858 . . . . 5 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ)
14847, 53, 69, 74, 147fprodcnv 11646 . . . 4 (𝜑 → ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
14941, 148eqtr4d 2223 . . 3 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
150 fprodcom2.1 . . . 4 (𝜑𝐴 ∈ Fin)
151 fprodcom2.3 . . . . . 6 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
152151ralrimiva 2560 . . . . 5 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
15325nfel1 2340 . . . . . 6 𝑗𝑥 / 𝑗𝐵 ∈ Fin
15428eleq1d 2256 . . . . . 6 (𝑗 = 𝑥 → (𝐵 ∈ Fin ↔ 𝑥 / 𝑗𝐵 ∈ Fin))
155153, 154rspc 2847 . . . . 5 (𝑥𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑥 / 𝑗𝐵 ∈ Fin))
156152, 155mpan9 281 . . . 4 ((𝜑𝑥𝐴) → 𝑥 / 𝑗𝐵 ∈ Fin)
15753, 150, 156, 125fprod2d 11644 . . 3 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
15847, 54, 62, 126fprod2d 11644 . . 3 (𝜑 → ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
159149, 157, 1583eqtr4d 2230 . 2 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
160 nfcv 2329 . . 3 𝑥𝑘𝐵 𝐸
161 nfcv 2329 . . . . 5 𝑗𝑦
162161, 111nfcsbw 3105 . . . 4 𝑗𝑦 / 𝑘𝑥 / 𝑗𝐸
16325, 162nfcprod 11576 . . 3 𝑗𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
164 nfcv 2329 . . . . 5 𝑦𝐸
165 nfcsb1v 3102 . . . . 5 𝑘𝑦 / 𝑘𝐸
166 csbeq1a 3078 . . . . 5 (𝑘 = 𝑦𝐸 = 𝑦 / 𝑘𝐸)
167164, 165, 166cbvprodi 11581 . . . 4 𝑘𝐵 𝐸 = ∏𝑦𝐵 𝑦 / 𝑘𝐸
168114csbeq2dv 3095 . . . . . 6 (𝑗 = 𝑥𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
169168adantr 276 . . . . 5 ((𝑗 = 𝑥𝑦𝐵) → 𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17028, 169prodeq12dv 11590 . . . 4 (𝑗 = 𝑥 → ∏𝑦𝐵 𝑦 / 𝑘𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
171167, 170eqtrid 2232 . . 3 (𝑗 = 𝑥 → ∏𝑘𝐵 𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
172160, 163, 171cbvprodi 11581 . 2 𝑗𝐴𝑘𝐵 𝐸 = ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
173 nfcv 2329 . . 3 𝑦𝑗𝐷 𝐸
17433, 119nfcprod 11576 . . 3 𝑘𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
175 nfcv 2329 . . . . 5 𝑥𝐸
176175, 111, 114cbvprodi 11581 . . . 4 𝑗𝐷 𝐸 = ∏𝑥𝐷 𝑥 / 𝑗𝐸
177121adantr 276 . . . . 5 ((𝑘 = 𝑦𝑥𝐷) → 𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17836, 177prodeq12dv 11590 . . . 4 (𝑘 = 𝑦 → ∏𝑥𝐷 𝑥 / 𝑗𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
179176, 178eqtrid 2232 . . 3 (𝑘 = 𝑦 → ∏𝑗𝐷 𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
180173, 174, 179cbvprodi 11581 . 2 𝑘𝐶𝑗𝐷 𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
181159, 172, 1803eqtr4g 2245 1 (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1363  wex 1502  wcel 2158  wral 2465  wrex 2466  Vcvv 2749  csb 3069  {csn 3604  cop 3607   ciun 3898  Disj wdisj 3992   × cxp 4636  ccnv 4637  Rel wrel 4643  cfv 5228  1st c1st 6152  2nd c2nd 6153  Fincfn 6753  cc 7822  cprod 11571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-disj 3993  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-frec 6405  df-1o 6430  df-oadd 6434  df-er 6548  df-en 6754  df-dom 6755  df-fin 6756  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-fz 10022  df-fzo 10156  df-seqfrec 10459  df-exp 10533  df-ihash 10769  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-clim 11300  df-proddc 11572
This theorem is referenced by:  fprodcom  11648  fprod0diagfz  11649
  Copyright terms: Public domain W3C validator