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

Theorem fprodcom2fi 11534
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 4697 . . . . . . . . 9 Rel ({𝑗} × 𝐵)
21rgenw 2512 . . . . . . . 8 𝑗𝐴 Rel ({𝑗} × 𝐵)
3 reliun 4709 . . . . . . . 8 (Rel 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐵))
42, 3mpbir 145 . . . . . . 7 Rel 𝑗𝐴 ({𝑗} × 𝐵)
5 relcnv 4966 . . . . . . 7 Rel 𝑘𝐶 ({𝑘} × 𝐷)
6 ancom 264 . . . . . . . . . . . 12 ((𝑥 = 𝑗𝑦 = 𝑘) ↔ (𝑦 = 𝑘𝑥 = 𝑗))
7 vex 2715 . . . . . . . . . . . . 13 𝑥 ∈ V
8 vex 2715 . . . . . . . . . . . . 13 𝑦 ∈ V
97, 8opth 4199 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ (𝑥 = 𝑗𝑦 = 𝑘))
108, 7opth 4199 . . . . . . . . . . . 12 (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ↔ (𝑦 = 𝑘𝑥 = 𝑗))
116, 9, 103bitr4i 211 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩)
1211a1i 9 . . . . . . . . . 10 (𝜑 → (⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩))
13 fprodcom2.4 . . . . . . . . . 10 (𝜑 → ((𝑗𝐴𝑘𝐵) ↔ (𝑘𝐶𝑗𝐷)))
1412, 13anbi12d 465 . . . . . . . . 9 (𝜑 → ((⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
15142exbidv 1848 . . . . . . . 8 (𝜑 → (∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷))))
16 eliunxp 4727 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝑘(⟨𝑥, 𝑦⟩ = ⟨𝑗, 𝑘⟩ ∧ (𝑗𝐴𝑘𝐵)))
177, 8opelcnv 4770 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
18 eliunxp 4727 . . . . . . . . 9 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
19 excom 1644 . . . . . . . . 9 (∃𝑘𝑗(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2017, 18, 193bitri 205 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗𝑘(⟨𝑦, 𝑥⟩ = ⟨𝑘, 𝑗⟩ ∧ (𝑘𝐶𝑗𝐷)))
2115, 16, 203bitr4g 222 . . . . . . 7 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷)))
224, 5, 21eqrelrdv 4684 . . . . . 6 (𝜑 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
23 nfcv 2299 . . . . . . 7 𝑥({𝑗} × 𝐵)
24 nfcv 2299 . . . . . . . 8 𝑗{𝑥}
25 nfcsb1v 3064 . . . . . . . 8 𝑗𝑥 / 𝑗𝐵
2624, 25nfxp 4615 . . . . . . 7 𝑗({𝑥} × 𝑥 / 𝑗𝐵)
27 sneq 3572 . . . . . . . 8 (𝑗 = 𝑥 → {𝑗} = {𝑥})
28 csbeq1a 3040 . . . . . . . 8 (𝑗 = 𝑥𝐵 = 𝑥 / 𝑗𝐵)
2927, 28xpeq12d 4613 . . . . . . 7 (𝑗 = 𝑥 → ({𝑗} × 𝐵) = ({𝑥} × 𝑥 / 𝑗𝐵))
3023, 26, 29cbviun 3888 . . . . . 6 𝑗𝐴 ({𝑗} × 𝐵) = 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)
31 nfcv 2299 . . . . . . . 8 𝑦({𝑘} × 𝐷)
32 nfcv 2299 . . . . . . . . 9 𝑘{𝑦}
33 nfcsb1v 3064 . . . . . . . . 9 𝑘𝑦 / 𝑘𝐷
3432, 33nfxp 4615 . . . . . . . 8 𝑘({𝑦} × 𝑦 / 𝑘𝐷)
35 sneq 3572 . . . . . . . . 9 (𝑘 = 𝑦 → {𝑘} = {𝑦})
36 csbeq1a 3040 . . . . . . . . 9 (𝑘 = 𝑦𝐷 = 𝑦 / 𝑘𝐷)
3735, 36xpeq12d 4613 . . . . . . . 8 (𝑘 = 𝑦 → ({𝑘} × 𝐷) = ({𝑦} × 𝑦 / 𝑘𝐷))
3831, 34, 37cbviun 3888 . . . . . . 7 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
3938cnveqi 4763 . . . . . 6 𝑘𝐶 ({𝑘} × 𝐷) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
4022, 30, 393eqtr3g 2213 . . . . 5 (𝜑 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵) = 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
4140prodeq1d 11472 . . . 4 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
428, 7op1std 6098 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) = 𝑦)
4342csbeq1d 3038 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸)
448, 7op2ndd 6099 . . . . . . . 8 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) = 𝑥)
4544csbeq1d 3038 . . . . . . 7 (𝑤 = ⟨𝑦, 𝑥⟩ → (2nd𝑤) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
4645csbeq2dv 3057 . . . . . 6 (𝑤 = ⟨𝑦, 𝑥⟩ → 𝑦 / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
4743, 46eqtrd 2190 . . . . 5 (𝑤 = ⟨𝑦, 𝑥⟩ → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
487, 8op2ndd 6099 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) = 𝑦)
4948csbeq1d 3038 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸)
507, 8op1std 6098 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
5150csbeq1d 3038 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) / 𝑗𝐸 = 𝑥 / 𝑗𝐸)
5251csbeq2dv 3057 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
5349, 52eqtrd 2190 . . . . 5 (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
54 fprodcom2.2 . . . . . 6 (𝜑𝐶 ∈ Fin)
55 snfig 6761 . . . . . . . . 9 (𝑦 ∈ V → {𝑦} ∈ Fin)
5655elv 2716 . . . . . . . 8 {𝑦} ∈ Fin
57 fprodcom2fi.d . . . . . . . . . 10 ((𝜑𝑘𝐶) → 𝐷 ∈ Fin)
5857ralrimiva 2530 . . . . . . . . 9 (𝜑 → ∀𝑘𝐶 𝐷 ∈ Fin)
5933nfel1 2310 . . . . . . . . . 10 𝑘𝑦 / 𝑘𝐷 ∈ Fin
6036eleq1d 2226 . . . . . . . . . 10 (𝑘 = 𝑦 → (𝐷 ∈ Fin ↔ 𝑦 / 𝑘𝐷 ∈ Fin))
6159, 60rspc 2810 . . . . . . . . 9 (𝑦𝐶 → (∀𝑘𝐶 𝐷 ∈ Fin → 𝑦 / 𝑘𝐷 ∈ Fin))
6258, 61mpan9 279 . . . . . . . 8 ((𝜑𝑦𝐶) → 𝑦 / 𝑘𝐷 ∈ Fin)
63 xpfi 6876 . . . . . . . 8 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑘𝐷 ∈ Fin) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6456, 62, 63sylancr 411 . . . . . . 7 ((𝜑𝑦𝐶) → ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6564ralrimiva 2530 . . . . . 6 (𝜑 → ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
66 disjsnxp 6186 . . . . . . 7 Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
6766a1i 9 . . . . . 6 (𝜑Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
68 iunfidisj 6892 . . . . . 6 ((𝐶 ∈ Fin ∧ ∀𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin ∧ Disj 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
6954, 65, 67, 68syl3anc 1220 . . . . 5 (𝜑 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ∈ Fin)
70 reliun 4709 . . . . . . 7 (Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∀𝑦𝐶 Rel ({𝑦} × 𝑦 / 𝑘𝐷))
71 relxp 4697 . . . . . . . 8 Rel ({𝑦} × 𝑦 / 𝑘𝐷)
7271a1i 9 . . . . . . 7 (𝑦𝐶 → Rel ({𝑦} × 𝑦 / 𝑘𝐷))
7370, 72mprgbir 2515 . . . . . 6 Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)
7473a1i 9 . . . . 5 (𝜑 → Rel 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
75 csbeq1 3034 . . . . . . . 8 (𝑥 = (2nd𝑤) → 𝑥 / 𝑗𝐸 = (2nd𝑤) / 𝑗𝐸)
7675csbeq2dv 3057 . . . . . . 7 (𝑥 = (2nd𝑤) → (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
7776eleq1d 2226 . . . . . 6 (𝑥 = (2nd𝑤) → ((1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ))
78 csbeq1 3034 . . . . . . . 8 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝐷 = (1st𝑤) / 𝑘𝐷)
79 csbeq1 3034 . . . . . . . . 9 (𝑦 = (1st𝑤) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 = (1st𝑤) / 𝑘𝑥 / 𝑗𝐸)
8079eleq1d 2226 . . . . . . . 8 (𝑦 = (1st𝑤) → (𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ (1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
8178, 80raleqbidv 2664 . . . . . . 7 (𝑦 = (1st𝑤) → (∀𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ ↔ ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
82 simpl 108 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝜑)
8333, 36opeliunxp2f 6187 . . . . . . . . . . . . . . 15 (⟨𝑦, 𝑥⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷) ↔ (𝑦𝐶𝑥𝑦 / 𝑘𝐷))
8417, 83sylbbr 135 . . . . . . . . . . . . . 14 ((𝑦𝐶𝑥𝑦 / 𝑘𝐷) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
8584adantl 275 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑘𝐶 ({𝑘} × 𝐷))
8622adantr 274 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑗𝐴 ({𝑗} × 𝐵) = 𝑘𝐶 ({𝑘} × 𝐷))
8785, 86eleqtrrd 2237 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵))
88 eliun 3855 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
8987, 88sylib 121 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → ∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
90 simpr 109 . . . . . . . . . . . . . . . 16 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵))
91 opelxp 4618 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) ↔ (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
9290, 91sylib 121 . . . . . . . . . . . . . . 15 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → (𝑥 ∈ {𝑗} ∧ 𝑦𝐵))
9392simpld 111 . . . . . . . . . . . . . 14 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ {𝑗})
94 elsni 3579 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑗} → 𝑥 = 𝑗)
9593, 94syl 14 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥 = 𝑗)
96 simpl 108 . . . . . . . . . . . . 13 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑗𝐴)
9795, 96eqeltrd 2234 . . . . . . . . . . . 12 ((𝑗𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵)) → 𝑥𝐴)
9897rexlimiva 2569 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑥𝐴)
9989, 98syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑥𝐴)
10025nfcri 2293 . . . . . . . . . . . 12 𝑗 𝑦𝑥 / 𝑗𝐵
10194equcomd 1687 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑗} → 𝑗 = 𝑥)
102101, 28syl 14 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑗} → 𝐵 = 𝑥 / 𝑗𝐵)
103102eleq2d 2227 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑗} → (𝑦𝐵𝑦𝑥 / 𝑗𝐵))
104103biimpa 294 . . . . . . . . . . . . . 14 ((𝑥 ∈ {𝑗} ∧ 𝑦𝐵) → 𝑦𝑥 / 𝑗𝐵)
10591, 104sylbi 120 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
106105a1i 9 . . . . . . . . . . . 12 (𝑗𝐴 → (⟨𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵))
107100, 106rexlimi 2567 . . . . . . . . . . 11 (∃𝑗𝐴𝑥, 𝑦⟩ ∈ ({𝑗} × 𝐵) → 𝑦𝑥 / 𝑗𝐵)
10889, 107syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦𝑥 / 𝑗𝐵)
109 fprodcom2.5 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐸 ∈ ℂ)
110109ralrimivva 2539 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ)
111 nfcsb1v 3064 . . . . . . . . . . . . . . . 16 𝑗𝑥 / 𝑗𝐸
112111nfel1 2310 . . . . . . . . . . . . . . 15 𝑗𝑥 / 𝑗𝐸 ∈ ℂ
11325, 112nfralw 2494 . . . . . . . . . . . . . 14 𝑗𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ
114 csbeq1a 3040 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑥𝐸 = 𝑥 / 𝑗𝐸)
115114eleq1d 2226 . . . . . . . . . . . . . . 15 (𝑗 = 𝑥 → (𝐸 ∈ ℂ ↔ 𝑥 / 𝑗𝐸 ∈ ℂ))
11628, 115raleqbidv 2664 . . . . . . . . . . . . . 14 (𝑗 = 𝑥 → (∀𝑘𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
117113, 116rspc 2810 . . . . . . . . . . . . 13 (𝑥𝐴 → (∀𝑗𝐴𝑘𝐵 𝐸 ∈ ℂ → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ))
118110, 117mpan9 279 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ)
119 nfcsb1v 3064 . . . . . . . . . . . . . 14 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸
120119nfel1 2310 . . . . . . . . . . . . 13 𝑘𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ
121 csbeq1a 3040 . . . . . . . . . . . . . 14 (𝑘 = 𝑦𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
122121eleq1d 2226 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (𝑥 / 𝑗𝐸 ∈ ℂ ↔ 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
123120, 122rspc 2810 . . . . . . . . . . . 12 (𝑦𝑥 / 𝑗𝐵 → (∀𝑘 𝑥 / 𝑗𝐵𝑥 / 𝑗𝐸 ∈ ℂ → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
124118, 123syl5com 29 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑦𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ))
125124impr 377 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝑥 / 𝑗𝐵)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
12682, 99, 108, 125syl12anc 1218 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐶𝑥𝑦 / 𝑘𝐷)) → 𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
127126ralrimivva 2539 . . . . . . . 8 (𝜑 → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
128127adantr 274 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
129 simpr 109 . . . . . . . . 9 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷))
130 eliun 3855 . . . . . . . . 9 (𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷) ↔ ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
131129, 130sylib 121 . . . . . . . 8 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷))
132 xp1st 6115 . . . . . . . . . . . 12 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ {𝑦})
133132adantl 275 . . . . . . . . . . 11 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ {𝑦})
134 elsni 3579 . . . . . . . . . . 11 ((1st𝑤) ∈ {𝑦} → (1st𝑤) = 𝑦)
135133, 134syl 14 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) = 𝑦)
136 simpl 108 . . . . . . . . . 10 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → 𝑦𝐶)
137135, 136eqeltrd 2234 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
138137rexlimiva 2569 . . . . . . . 8 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (1st𝑤) ∈ 𝐶)
139131, 138syl 14 . . . . . . 7 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) ∈ 𝐶)
14081, 128, 139rspcdva 2821 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → ∀𝑥 (1st𝑤) / 𝑘𝐷(1st𝑤) / 𝑘𝑥 / 𝑗𝐸 ∈ ℂ)
141 xp2nd 6116 . . . . . . . . . 10 (𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
142141adantl 275 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ 𝑦 / 𝑘𝐷)
143135csbeq1d 3038 . . . . . . . . 9 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘𝐷 = 𝑦 / 𝑘𝐷)
144142, 143eleqtrrd 2237 . . . . . . . 8 ((𝑦𝐶𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
145144rexlimiva 2569 . . . . . . 7 (∃𝑦𝐶 𝑤 ∈ ({𝑦} × 𝑦 / 𝑘𝐷) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
146131, 145syl 14 . . . . . 6 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (2nd𝑤) ∈ (1st𝑤) / 𝑘𝐷)
14777, 140, 146rspcdva 2821 . . . . 5 ((𝜑𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)) → (1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 ∈ ℂ)
14847, 53, 69, 74, 147fprodcnv 11533 . . . 4 (𝜑 → ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸 = ∏𝑧 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
14941, 148eqtr4d 2193 . . 3 (𝜑 → ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
150 fprodcom2.1 . . . 4 (𝜑𝐴 ∈ Fin)
151 fprodcom2.3 . . . . . 6 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
152151ralrimiva 2530 . . . . 5 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
15325nfel1 2310 . . . . . 6 𝑗𝑥 / 𝑗𝐵 ∈ Fin
15428eleq1d 2226 . . . . . 6 (𝑗 = 𝑥 → (𝐵 ∈ Fin ↔ 𝑥 / 𝑗𝐵 ∈ Fin))
155153, 154rspc 2810 . . . . 5 (𝑥𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑥 / 𝑗𝐵 ∈ Fin))
156152, 155mpan9 279 . . . 4 ((𝜑𝑥𝐴) → 𝑥 / 𝑗𝐵 ∈ Fin)
15753, 150, 156, 125fprod2d 11531 . . 3 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑧 𝑥𝐴 ({𝑥} × 𝑥 / 𝑗𝐵)(2nd𝑧) / 𝑘(1st𝑧) / 𝑗𝐸)
15847, 54, 62, 126fprod2d 11531 . . 3 (𝜑 → ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑤 𝑦𝐶 ({𝑦} × 𝑦 / 𝑘𝐷)(1st𝑤) / 𝑘(2nd𝑤) / 𝑗𝐸)
159149, 157, 1583eqtr4d 2200 . 2 (𝜑 → ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
160 nfcv 2299 . . 3 𝑥𝑘𝐵 𝐸
161 nfcv 2299 . . . . 5 𝑗𝑦
162161, 111nfcsbw 3067 . . . 4 𝑗𝑦 / 𝑘𝑥 / 𝑗𝐸
16325, 162nfcprod 11463 . . 3 𝑗𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
164 nfcv 2299 . . . . 5 𝑦𝐸
165 nfcsb1v 3064 . . . . 5 𝑘𝑦 / 𝑘𝐸
166 csbeq1a 3040 . . . . 5 (𝑘 = 𝑦𝐸 = 𝑦 / 𝑘𝐸)
167164, 165, 166cbvprodi 11468 . . . 4 𝑘𝐵 𝐸 = ∏𝑦𝐵 𝑦 / 𝑘𝐸
168114csbeq2dv 3057 . . . . . 6 (𝑗 = 𝑥𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
169168adantr 274 . . . . 5 ((𝑗 = 𝑥𝑦𝐵) → 𝑦 / 𝑘𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17028, 169prodeq12dv 11477 . . . 4 (𝑗 = 𝑥 → ∏𝑦𝐵 𝑦 / 𝑘𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
171167, 170syl5eq 2202 . . 3 (𝑗 = 𝑥 → ∏𝑘𝐵 𝐸 = ∏𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸)
172160, 163, 171cbvprodi 11468 . 2 𝑗𝐴𝑘𝐵 𝐸 = ∏𝑥𝐴𝑦 𝑥 / 𝑗𝐵𝑦 / 𝑘𝑥 / 𝑗𝐸
173 nfcv 2299 . . 3 𝑦𝑗𝐷 𝐸
17433, 119nfcprod 11463 . . 3 𝑘𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
175 nfcv 2299 . . . . 5 𝑥𝐸
176175, 111, 114cbvprodi 11468 . . . 4 𝑗𝐷 𝐸 = ∏𝑥𝐷 𝑥 / 𝑗𝐸
177121adantr 274 . . . . 5 ((𝑘 = 𝑦𝑥𝐷) → 𝑥 / 𝑗𝐸 = 𝑦 / 𝑘𝑥 / 𝑗𝐸)
17836, 177prodeq12dv 11477 . . . 4 (𝑘 = 𝑦 → ∏𝑥𝐷 𝑥 / 𝑗𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
179176, 178syl5eq 2202 . . 3 (𝑘 = 𝑦 → ∏𝑗𝐷 𝐸 = ∏𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸)
180173, 174, 179cbvprodi 11468 . 2 𝑘𝐶𝑗𝐷 𝐸 = ∏𝑦𝐶𝑥 𝑦 / 𝑘𝐷𝑦 / 𝑘𝑥 / 𝑗𝐸
181159, 172, 1803eqtr4g 2215 1 (𝜑 → ∏𝑗𝐴𝑘𝐵 𝐸 = ∏𝑘𝐶𝑗𝐷 𝐸)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1335  wex 1472  wcel 2128  wral 2435  wrex 2436  Vcvv 2712  csb 3031  {csn 3561  cop 3564   ciun 3851  Disj wdisj 3944   × cxp 4586  ccnv 4587  Rel wrel 4593  cfv 5172  1st c1st 6088  2nd c2nd 6089  Fincfn 6687  cc 7732  cprod 11458
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4081  ax-sep 4084  ax-nul 4092  ax-pow 4137  ax-pr 4171  ax-un 4395  ax-setind 4498  ax-iinf 4549  ax-cnex 7825  ax-resscn 7826  ax-1cn 7827  ax-1re 7828  ax-icn 7829  ax-addcl 7830  ax-addrcl 7831  ax-mulcl 7832  ax-mulrcl 7833  ax-addcom 7834  ax-mulcom 7835  ax-addass 7836  ax-mulass 7837  ax-distr 7838  ax-i2m1 7839  ax-0lt1 7840  ax-1rid 7841  ax-0id 7842  ax-rnegex 7843  ax-precex 7844  ax-cnre 7845  ax-pre-ltirr 7846  ax-pre-ltwlin 7847  ax-pre-lttrn 7848  ax-pre-apti 7849  ax-pre-ltadd 7850  ax-pre-mulgt0 7851  ax-pre-mulext 7852  ax-arch 7853  ax-caucvg 7854
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3396  df-if 3507  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-int 3810  df-iun 3853  df-disj 3945  df-br 3968  df-opab 4028  df-mpt 4029  df-tr 4065  df-id 4255  df-po 4258  df-iso 4259  df-iord 4328  df-on 4330  df-ilim 4331  df-suc 4333  df-iom 4552  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-iota 5137  df-fun 5174  df-fn 5175  df-f 5176  df-f1 5177  df-fo 5178  df-f1o 5179  df-fv 5180  df-isom 5181  df-riota 5782  df-ov 5829  df-oprab 5830  df-mpo 5831  df-1st 6090  df-2nd 6091  df-recs 6254  df-irdg 6319  df-frec 6340  df-1o 6365  df-oadd 6369  df-er 6482  df-en 6688  df-dom 6689  df-fin 6690  df-pnf 7916  df-mnf 7917  df-xr 7918  df-ltxr 7919  df-le 7920  df-sub 8052  df-neg 8053  df-reap 8454  df-ap 8461  df-div 8550  df-inn 8839  df-2 8897  df-3 8898  df-4 8899  df-n0 9096  df-z 9173  df-uz 9445  df-q 9535  df-rp 9567  df-fz 9919  df-fzo 10051  df-seqfrec 10354  df-exp 10428  df-ihash 10661  df-cj 10753  df-re 10754  df-im 10755  df-rsqrt 10909  df-abs 10910  df-clim 11187  df-proddc 11459
This theorem is referenced by:  fprodcom  11535  fprod0diagfz  11536
  Copyright terms: Public domain W3C validator