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

Theorem fprodcom2fi 11589
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 4720 . . . . . . . . 9 Rel ({𝑗} × 𝐵)
21rgenw 2525 . . . . . . . 8 𝑗𝐴 Rel ({𝑗} × 𝐵)
3 reliun 4732 . . . . . . . 8 (Rel 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐵))
42, 3mpbir 145 . . . . . . 7 Rel 𝑗𝐴 ({𝑗} × 𝐵)
5 relcnv 4989 . . . . . . 7 Rel 𝑘𝐶 ({𝑘} × 𝐷)
6 ancom 264 . . . . . . . . . . . 12 ((𝑥 = 𝑗𝑦 = 𝑘) ↔ (𝑦 = 𝑘𝑥 = 𝑗))
7 vex 2733 . . . . . . . . . . . . 13 𝑥 ∈ V
8 vex 2733 . . . . . . . . . . . . 13 𝑦 ∈ V
97, 8opth 4222 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ (𝑥 = 𝑗𝑦 = 𝑘))
108, 7opth 4222 . . . . . . . . . . . 12 (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ↔ (𝑦 = 𝑘𝑥 = 𝑗))
116, 9, 103bitr4i 211 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩)
1211a1i 9 . . . . . . . . . 10 (𝜑 → (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩))
13 fprodcom2.4 . . . . . . . . . 10 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
1412, 13anbi12d 470 . . . . . . . . 9 (𝜑 → ((⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
15142exbidv 1861 . . . . . . . 8 (𝜑 → (∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
16 eliunxp 4750 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)))
177, 8opelcnv 4793 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
18 eliunxp 4750 . . . . . . . . 9 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
19 excom 1657 . . . . . . . . 9 (∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2017, 18, 193bitri 205 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2115, 16, 203bitr4g 222 . . . . . . 7 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷)))
224, 5, 21eqrelrdv 4707 . . . . . 6 (𝜑 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
23 nfcv 2312 . . . . . . 7 𝑥({𝑗} × 𝐵)
24 nfcv 2312 . . . . . . . 8 𝑗{𝑥}
25 nfcsb1v 3082 . . . . . . . 8 𝑗𝑥 / 𝑗𝐵
2624, 25nfxp 4638 . . . . . . 7 𝑗({𝑥} × 𝑥 / 𝑗𝐵)
27 sneq 3594 . . . . . . . 8 (𝑗 = 𝑥 → {𝑗} = {𝑥})
28 csbeq1a 3058 . . . . . . . 8 (𝑗 = 𝑥𝐵 = 𝑥 / 𝑗𝐵)
2927, 28xpeq12d 4636 . . . . . . 7 (𝑗 = 𝑥 → ({𝑗} × 𝐵) = ({𝑥} × 𝑥 / 𝑗𝐵))
3023, 26, 29cbviun 3910 . . . . . 6 𝑗𝐴 ({𝑗} × 𝐵) = 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)
31 nfcv 2312 . . . . . . . 8 𝑦({𝑘} × 𝐷)
32 nfcv 2312 . . . . . . . . 9 𝑘{𝑦}
33 nfcsb1v 3082 . . . . . . . . 9 𝑘𝑦 / 𝑘𝐷
3432, 33nfxp 4638 . . . . . . . 8 𝑘({𝑦} × 𝑦 / 𝑘𝐷)
35 sneq 3594 . . . . . . . . 9 (𝑘 = 𝑦 → {𝑘} = {𝑦})
36 csbeq1a 3058 . . . . . . . . 9 (𝑘 = 𝑦𝐷 = 𝑦 / 𝑘𝐷)
3735, 36xpeq12d 4636 . . . . . . . 8 (𝑘 = 𝑦 → ({𝑘} × 𝐷) = ({𝑦} × 𝑦 / 𝑘𝐷))
3831, 34, 37cbviun 3910 . . . . . . 7 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
3938cnveqi 4786 . . . . . 6 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
4022, 30, 393eqtr3g 2226 . . . . 5 (𝜑 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
4140prodeq1d 11527 . . . 4 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
428, 7op1std 6127 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) = 𝑦)
4342csbeq1d 3056 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸)
448, 7op2ndd 6128 . . . . . . . 8 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) = 𝑥)
4544csbeq1d 3056 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
4645csbeq2dv 3075 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
4743, 46eqtrd 2203 . . . . 5 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
487, 8op2ndd 6128 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
4948csbeq1d 3056 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸)
507, 8op1std 6127 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5150csbeq1d 3056 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
5251csbeq2dv 3075 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
5349, 52eqtrd 2203 . . . . 5 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
54 fprodcom2.2 . . . . . 6 (𝜑𝐶 ∈ Fin)
55 snfig 6792 . . . . . . . . 9 (𝑦 ∈ V → {𝑦} ∈ Fin)
5655elv 2734 . . . . . . . 8 {𝑦} ∈ Fin
57 fprodcom2fi.d . . . . . . . . . 10 ((𝜑𝑘𝐶) → 𝐷 ∈ Fin)
5857ralrimiva 2543 . . . . . . . . 9 (𝜑 → ∀𝑘𝐶 𝐷 ∈ Fin)
5933nfel1 2323 . . . . . . . . . 10 𝑘𝑦 / 𝑘𝐷 ∈ Fin
6036eleq1d 2239 . . . . . . . . . 10 (𝑘 = 𝑦 → (𝐷 ∈ Fin ↔ 𝑦 / 𝑘𝐷 ∈ Fin))
6159, 60rspc 2828 . . . . . . . . 9 (𝑦𝐶 → (∀𝑘𝐶 𝐷 ∈ Fin → 𝑦 / 𝑘𝐷 ∈ Fin))
6258, 61mpan9 279 . . . . . . . 8 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷 ∈ Fin)
63 xpfi 6907 . . . . . . . 8 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑘𝐷 ∈ Fin) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6456, 62, 63sylancr 412 . . . . . . 7 ((𝜑𝑦𝐶) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6564ralrimiva 2543 . . . . . 6 (𝜑 → ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
66 disjsnxp 6216 . . . . . . 7 Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
6766a1i 9 . . . . . 6 (𝜑Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
68 iunfidisj 6923 . . . . . 6 ((𝐶 ∈ Fin ∧ ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin ∧ Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6954, 65, 67, 68syl3anc 1233 . . . . 5 (𝜑 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
70 reliun 4732 . . . . . . 7 (Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∀𝑦𝐶 Rel ({𝑦} × 𝑦 / 𝑘𝐷))
71 relxp 4720 . . . . . . . 8 Rel ({𝑦} × 𝑦 / 𝑘𝐷)
7271a1i 9 . . . . . . 7 (𝑦𝐶 → Rel ({𝑦} × 𝑦 / 𝑘𝐷))
7370, 72mprgbir 2528 . . . . . 6 Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
7473a1i 9 . . . . 5 (𝜑 → Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
75 csbeq1 3052 . . . . . . . 8 (𝑥 = (2nd𝑤) → 𝑥 / 𝑗𝐸 = (2nd𝑤) / 𝑗𝐸)
7675csbeq2dv 3075 . . . . . . 7 (𝑥 = (2nd𝑤) → (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
7776eleq1d 2239 . . . . . 6 (𝑥 = (2nd𝑤) → ((1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ))
78 csbeq1 3052 . . . . . . . 8 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝐷 = (1st𝑤) / 𝑘𝐷)
79 csbeq1 3052 . . . . . . . . 9 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘𝑥 / 𝑗𝐸)
8079eleq1d 2239 . . . . . . . 8 (𝑦 = (1st𝑤) → (𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
8178, 80raleqbidv 2677 . . . . . . 7 (𝑦 = (1st𝑤) → (∀𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
82 simpl 108 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝜑)
8333, 36opeliunxp2f 6217 . . . . . . . . . . . . . . 15 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ (𝑦𝐶𝑥𝑦 / 𝑘𝐷))
8417, 83sylbbr 135 . . . . . . . . . . . . . 14 ((𝑦𝐶𝑥𝑦 / 𝑘𝐷) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
8584adantl 275 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
8622adantr 274 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
8785, 86eleqtrrd 2250 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵))
88 eliun 3877 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
8987, 88sylib 121 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
90 simpr 109 . . . . . . . . . . . . . . . 16 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
91 opelxp 4641 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) ↔ (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
9290, 91sylib 121 . . . . . . . . . . . . . . 15 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
9392simpld 111 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ {𝑗})
94 elsni 3601 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑗} → 𝑥 = 𝑗)
9593, 94syl 14 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 = 𝑗)
96 simpl 108 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑗𝐴)
9795, 96eqeltrd 2247 . . . . . . . . . . . 12 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥𝐴)
9897rexlimiva 2582 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑥𝐴)
9989, 98syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑥𝐴)
10025nfcri 2306 . . . . . . . . . . . 12 𝑗 𝑦𝑥 / 𝑗𝐵
10194equcomd 1700 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑗} → 𝑗 = 𝑥)
102101, 28syl 14 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑗} → 𝐵 = 𝑥 / 𝑗𝐵)
103102eleq2d 2240 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → (𝑦𝐵𝑦𝑥 / 𝑗𝐵))
104103biimpa 294 . . . . . . . . . . . . . 14 ((𝑥 ∈ {𝑗} ∧ 𝑦𝐵) → 𝑦𝑥 / 𝑗𝐵)
10591, 104sylbi 120 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
106105a1i 9 . . . . . . . . . . . 12 (𝑗𝐴 → (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵))
107100, 106rexlimi 2580 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
10889, 107syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦𝑥 / 𝑗𝐵)
109 fprodcom2.5 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
110109ralrimivva 2552 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ)
111 nfcsb1v 3082 . . . . . . . . . . . . . . . 16 𝑗𝑥 / 𝑗𝐸
112111nfel1 2323 . . . . . . . . . . . . . . 15 𝑗𝑥 / 𝑗𝐸 ∈ ℂ
11325, 112nfralw 2507 . . . . . . . . . . . . . 14 𝑗𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ
114 csbeq1a 3058 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑥𝐸 = 𝑥 / 𝑗𝐸)
115114eleq1d 2239 . . . . . . . . . . . . . . 15 (𝑗 = 𝑥 → (𝐸 ∈ ℂ ↔ 𝑥 / 𝑗𝐸 ∈ ℂ))
11628, 115raleqbidv 2677 . . . . . . . . . . . . . 14 (𝑗 = 𝑥 → (∀𝑘𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
117113, 116rspc 2828 . . . . . . . . . . . . 13 (𝑥𝐴 → (∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
118110, 117mpan9 279 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ)
119 nfcsb1v 3082 . . . . . . . . . . . . . 14 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸
120119nfel1 2323 . . . . . . . . . . . . 13 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ
121 csbeq1a 3058 . . . . . . . . . . . . . 14 (𝑘 = 𝑦𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
122121eleq1d 2239 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (𝑥 / 𝑗𝐸 ∈ ℂ ↔ 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
123120, 122rspc 2828 . . . . . . . . . . . 12 (𝑦𝑥 / 𝑗𝐵 → (∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
124118, 123syl5com 29 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑦𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
125124impr 377 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝑥 / 𝑗𝐵)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
12682, 99, 108, 125syl12anc 1231 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
127126ralrimivva 2552 . . . . . . . 8 (𝜑 → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
128127adantr 274 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
129 simpr 109 . . . . . . . . 9 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
130 eliun 3877 . . . . . . . . 9 (𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
131129, 130sylib 121 . . . . . . . 8 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
132 xp1st 6144 . . . . . . . . . . . 12 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ {𝑦})
133132adantl 275 . . . . . . . . . . 11 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ {𝑦})
134 elsni 3601 . . . . . . . . . . 11 ((1st𝑤) ∈ {𝑦} → (1st𝑤) = 𝑦)
135133, 134syl 14 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) = 𝑦)
136 simpl 108 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶)
137135, 136eqeltrd 2247 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
138137rexlimiva 2582 . . . . . . . 8 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ 𝐶)
139131, 138syl 14 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
14081, 128, 139rspcdva 2839 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
141 xp2nd 6145 . . . . . . . . . 10 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
142141adantl 275 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
143135csbeq1d 3056 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘𝐷 = 𝑦 / 𝑘𝐷)
144142, 143eleqtrrd 2250 . . . . . . . 8 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
145144rexlimiva 2582 . . . . . . 7 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
146131, 145syl 14 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
14777, 140, 146rspcdva 2839 . . . . 5 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ)
14847, 53, 69, 74, 147fprodcnv 11588 . . . 4 (𝜑 → ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
14941, 148eqtr4d 2206 . . 3 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
150 fprodcom2.1 . . . 4 (𝜑𝐴 ∈ Fin)
151 fprodcom2.3 . . . . . 6 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
152151ralrimiva 2543 . . . . 5 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
15325nfel1 2323 . . . . . 6 𝑗𝑥 / 𝑗𝐵 ∈ Fin
15428eleq1d 2239 . . . . . 6 (𝑗 = 𝑥 → (𝐵 ∈ Fin ↔ 𝑥 / 𝑗𝐵 ∈ Fin))
155153, 154rspc 2828 . . . . 5 (𝑥𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑥 / 𝑗𝐵 ∈ Fin))
156152, 155mpan9 279 . . . 4 ((𝜑𝑥𝐴) → 𝑥 / 𝑗𝐵 ∈ Fin)
15753, 150, 156, 125fprod2d 11586 . . 3 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
15847, 54, 62, 126fprod2d 11586 . . 3 (𝜑 → ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
159149, 157, 1583eqtr4d 2213 . 2 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
160 nfcv 2312 . . 3 𝑥𝑘𝐵 𝐸
161 nfcv 2312 . . . . 5 𝑗𝑦
162161, 111nfcsbw 3085 . . . 4 𝑗𝑦 / 𝑘𝑥 / 𝑗𝐸
16325, 162nfcprod 11518 . . 3 𝑗𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
164 nfcv 2312 . . . . 5 𝑦𝐸
165 nfcsb1v 3082 . . . . 5 𝑘𝑦 / 𝑘𝐸
166 csbeq1a 3058 . . . . 5 (𝑘 = 𝑦𝐸 = 𝑦 / 𝑘𝐸)
167164, 165, 166cbvprodi 11523 . . . 4 𝑘𝐵 𝐸 = ∏𝑦𝐵 𝑦 / 𝑘𝐸
168114csbeq2dv 3075 . . . . . 6 (𝑗 = 𝑥𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
169168adantr 274 . . . . 5 ((𝑗 = 𝑥𝑦𝐵) → 𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17028, 169prodeq12dv 11532 . . . 4 (𝑗 = 𝑥 → ∏𝑦𝐵 𝑦 / 𝑘𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
171167, 170eqtrid 2215 . . 3 (𝑗 = 𝑥 → ∏𝑘𝐵 𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
172160, 163, 171cbvprodi 11523 . 2 𝑗𝐴𝑘𝐵 𝐸 = ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
173 nfcv 2312 . . 3 𝑦𝑗𝐷 𝐸
17433, 119nfcprod 11518 . . 3 𝑘𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
175 nfcv 2312 . . . . 5 𝑥𝐸
176175, 111, 114cbvprodi 11523 . . . 4 𝑗𝐷 𝐸 = ∏𝑥𝐷 𝑥 / 𝑗𝐸
177121adantr 274 . . . . 5 ((𝑘 = 𝑦𝑥𝐷) → 𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17836, 177prodeq12dv 11532 . . . 4 (𝑘 = 𝑦 → ∏𝑥𝐷 𝑥 / 𝑗𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
179176, 178eqtrid 2215 . . 3 (𝑘 = 𝑦 → ∏𝑗𝐷 𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
180173, 174, 179cbvprodi 11523 . 2 𝑘𝐶𝑗𝐷 𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
181159, 172, 1803eqtr4g 2228 1 (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1348  wex 1485  wcel 2141  wral 2448  wrex 2449  Vcvv 2730  csb 3049  {csn 3583  cop 3586   ciun 3873  Disj wdisj 3966   × cxp 4609  ccnv 4610  Rel wrel 4616  cfv 5198  1st c1st 6117  2nd c2nd 6118  Fincfn 6718  cc 7772  cprod 11513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892  ax-arch 7893  ax-caucvg 7894
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-disj 3967  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-isom 5207  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-frec 6370  df-1o 6395  df-oadd 6399  df-er 6513  df-en 6719  df-dom 6720  df-fin 6721  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-3 8938  df-4 8939  df-n0 9136  df-z 9213  df-uz 9488  df-q 9579  df-rp 9611  df-fz 9966  df-fzo 10099  df-seqfrec 10402  df-exp 10476  df-ihash 10710  df-cj 10806  df-re 10807  df-im 10808  df-rsqrt 10962  df-abs 10963  df-clim 11242  df-proddc 11514
This theorem is referenced by:  fprodcom  11590  fprod0diagfz  11591
  Copyright terms: Public domain W3C validator