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

Theorem fprod2dlemstep 11644
Description: Lemma for fprod2d 11645- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)
Hypotheses
Ref Expression
fprod2d.1 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
fprod2d.2 (𝜑𝐴 ∈ Fin)
fprod2d.3 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
fprod2d.4 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
fprod2d.5 (𝜑 → ¬ 𝑦𝑥)
fprod2d.6 (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
fprod2dlemstep.x (𝜑𝑥 ∈ Fin)
fprod2d.7 (𝜓 ↔ ∏𝑗𝑥𝑘𝐵 𝐶 = ∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
Assertion
Ref Expression
fprod2dlemstep ((𝜑𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑘,𝑧   𝑧,𝐶   𝐷,𝑗,𝑘   𝜑,𝑗   𝑥,𝑗   𝑦,𝑗,𝑧   𝜑,𝑘   𝑥,𝑘   𝑦,𝑘,𝑧   𝜑,𝑧   𝑥,𝑧   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦,𝑧,𝑗,𝑘)   𝐴(𝑥,𝑦,𝑧)   𝐵(𝑥,𝑦,𝑗)   𝐶(𝑥,𝑦,𝑗,𝑘)   𝐷(𝑥,𝑦,𝑧)

Proof of Theorem fprod2dlemstep
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . 4 ((𝜑𝜓) → 𝜓)
2 fprod2d.7 . . . 4 (𝜓 ↔ ∏𝑗𝑥𝑘𝐵 𝐶 = ∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
31, 2sylib 122 . . 3 ((𝜑𝜓) → ∏𝑗𝑥𝑘𝐵 𝐶 = ∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
4 nfcv 2329 . . . . . 6 𝑚𝑘𝐵 𝐶
5 nfcsb1v 3102 . . . . . . 7 𝑗𝑚 / 𝑗𝐵
6 nfcsb1v 3102 . . . . . . 7 𝑗𝑚 / 𝑗𝐶
75, 6nfcprod 11577 . . . . . 6 𝑗𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
8 csbeq1a 3078 . . . . . . 7 (𝑗 = 𝑚𝐵 = 𝑚 / 𝑗𝐵)
9 csbeq1a 3078 . . . . . . . 8 (𝑗 = 𝑚𝐶 = 𝑚 / 𝑗𝐶)
109adantr 276 . . . . . . 7 ((𝑗 = 𝑚𝑘𝐵) → 𝐶 = 𝑚 / 𝑗𝐶)
118, 10prodeq12dv 11591 . . . . . 6 (𝑗 = 𝑚 → ∏𝑘𝐵 𝐶 = ∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶)
124, 7, 11cbvprodi 11582 . . . . 5 𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶 = ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
13 fprod2d.6 . . . . . . . . 9 (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
1413unssbd 3325 . . . . . . . 8 (𝜑 → {𝑦} ⊆ 𝐴)
15 vex 2752 . . . . . . . . 9 𝑦 ∈ V
1615snss 3739 . . . . . . . 8 (𝑦𝐴 ↔ {𝑦} ⊆ 𝐴)
1714, 16sylibr 134 . . . . . . 7 (𝜑𝑦𝐴)
18 fprod2d.3 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
1918ralrimiva 2560 . . . . . . . . 9 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
20 nfcsb1v 3102 . . . . . . . . . . 11 𝑗𝑦 / 𝑗𝐵
2120nfel1 2340 . . . . . . . . . 10 𝑗𝑦 / 𝑗𝐵 ∈ Fin
22 csbeq1a 3078 . . . . . . . . . . 11 (𝑗 = 𝑦𝐵 = 𝑦 / 𝑗𝐵)
2322eleq1d 2256 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ 𝑦 / 𝑗𝐵 ∈ Fin))
2421, 23rspc 2847 . . . . . . . . 9 (𝑦𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑦 / 𝑗𝐵 ∈ Fin))
2517, 19, 24sylc 62 . . . . . . . 8 (𝜑𝑦 / 𝑗𝐵 ∈ Fin)
26 fprod2d.4 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
2726ralrimivva 2569 . . . . . . . . . 10 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ)
28 nfcsb1v 3102 . . . . . . . . . . . . 13 𝑗𝑦 / 𝑗𝐶
2928nfel1 2340 . . . . . . . . . . . 12 𝑗𝑦 / 𝑗𝐶 ∈ ℂ
3020, 29nfralw 2524 . . . . . . . . . . 11 𝑗𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ
31 csbeq1a 3078 . . . . . . . . . . . . 13 (𝑗 = 𝑦𝐶 = 𝑦 / 𝑗𝐶)
3231eleq1d 2256 . . . . . . . . . . . 12 (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ 𝑦 / 𝑗𝐶 ∈ ℂ))
3322, 32raleqbidv 2695 . . . . . . . . . . 11 (𝑗 = 𝑦 → (∀𝑘𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3430, 33rspc 2847 . . . . . . . . . 10 (𝑦𝐴 → (∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3517, 27, 34sylc 62 . . . . . . . . 9 (𝜑 → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
3635r19.21bi 2575 . . . . . . . 8 ((𝜑𝑘𝑦 / 𝑗𝐵) → 𝑦 / 𝑗𝐶 ∈ ℂ)
3725, 36fprodcl 11629 . . . . . . 7 (𝜑 → ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
38 csbeq1 3072 . . . . . . . . 9 (𝑚 = 𝑦𝑚 / 𝑗𝐵 = 𝑦 / 𝑗𝐵)
39 csbeq1 3072 . . . . . . . . . 10 (𝑚 = 𝑦𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4039adantr 276 . . . . . . . . 9 ((𝑚 = 𝑦𝑘𝑚 / 𝑗𝐵) → 𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4138, 40prodeq12dv 11591 . . . . . . . 8 (𝑚 = 𝑦 → ∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4241prodsn 11615 . . . . . . 7 ((𝑦𝐴 ∧ ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ) → ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4317, 37, 42syl2anc 411 . . . . . 6 (𝜑 → ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
44 nfcv 2329 . . . . . . . 8 𝑚𝑦 / 𝑗𝐶
45 nfcsb1v 3102 . . . . . . . 8 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶
46 csbeq1a 3078 . . . . . . . 8 (𝑘 = 𝑚𝑦 / 𝑗𝐶 = 𝑚 / 𝑘𝑦 / 𝑗𝐶)
4744, 45, 46cbvprodi 11582 . . . . . . 7 𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = ∏𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶
48 csbeq1 3072 . . . . . . . . 9 (𝑚 = (2nd𝑧) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
49 snfig 6828 . . . . . . . . . . 11 (𝑦 ∈ V → {𝑦} ∈ Fin)
5049elv 2753 . . . . . . . . . 10 {𝑦} ∈ Fin
51 xpfi 6943 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑗𝐵 ∈ Fin) → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
5250, 25, 51sylancr 414 . . . . . . . . 9 (𝜑 → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
53 2ndconst 6237 . . . . . . . . . 10 (𝑦𝐴 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
5417, 53syl 14 . . . . . . . . 9 (𝜑 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
55 fvres 5551 . . . . . . . . . 10 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5655adantl 277 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5745nfel1 2340 . . . . . . . . . . 11 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ
5846eleq1d 2256 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝑦 / 𝑗𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
5957, 58rspc 2847 . . . . . . . . . 10 (𝑚𝑦 / 𝑗𝐵 → (∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
6035, 59mpan9 281 . . . . . . . . 9 ((𝜑𝑚𝑦 / 𝑗𝐵) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ)
6148, 52, 54, 56, 60fprodf1o 11610 . . . . . . . 8 (𝜑 → ∏𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
62 elxp 4655 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)))
63 nfv 1538 . . . . . . . . . . . . . . 15 𝑗 𝑧 = ⟨𝑚, 𝑘
64 nfv 1538 . . . . . . . . . . . . . . . 16 𝑗 𝑚 ∈ {𝑦}
6520nfcri 2323 . . . . . . . . . . . . . . . 16 𝑗 𝑘𝑦 / 𝑗𝐵
6664, 65nfan 1575 . . . . . . . . . . . . . . 15 𝑗(𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)
6763, 66nfan 1575 . . . . . . . . . . . . . 14 𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
6867nfex 1647 . . . . . . . . . . . . 13 𝑗𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
69 nfv 1538 . . . . . . . . . . . . 13 𝑚𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))
70 opeq1 3790 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
7170eqeq2d 2199 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
72 eleq1w 2248 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑗 → (𝑚 ∈ {𝑦} ↔ 𝑗 ∈ {𝑦}))
73 velsn 3621 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
7472, 73bitrdi 196 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → (𝑚 ∈ {𝑦} ↔ 𝑗 = 𝑦))
7574anbi1d 465 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑗 = 𝑦𝑘𝑦 / 𝑗𝐵)))
7622eleq2d 2257 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑦 → (𝑘𝐵𝑘𝑦 / 𝑗𝐵))
7776pm5.32i 454 . . . . . . . . . . . . . . . 16 ((𝑗 = 𝑦𝑘𝐵) ↔ (𝑗 = 𝑦𝑘𝑦 / 𝑗𝐵))
7875, 77bitr4di 198 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑗 = 𝑦𝑘𝐵)))
7971, 78anbi12d 473 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8079exbidv 1835 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8168, 69, 80cbvexv1 1762 . . . . . . . . . . . 12 (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
8262, 81bitri 184 . . . . . . . . . . 11 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
83 nfv 1538 . . . . . . . . . . . 12 𝑗𝜑
84 nfcv 2329 . . . . . . . . . . . . . 14 𝑗(2nd𝑧)
8584, 28nfcsbw 3105 . . . . . . . . . . . . 13 𝑗(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
8685nfeq2 2341 . . . . . . . . . . . 12 𝑗 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
87 nfv 1538 . . . . . . . . . . . . 13 𝑘𝜑
88 nfcsb1v 3102 . . . . . . . . . . . . . 14 𝑘(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
8988nfeq2 2341 . . . . . . . . . . . . 13 𝑘 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
90 fprod2d.1 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
9190ad2antlr 489 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = 𝐶)
9231ad2antrl 490 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐶 = 𝑦 / 𝑗𝐶)
93 fveq2 5527 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
94 vex 2752 . . . . . . . . . . . . . . . . . . 19 𝑗 ∈ V
95 vex 2752 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
9694, 95op2nd 6162 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
9793, 96eqtr2di 2237 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd𝑧))
9897ad2antlr 489 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑘 = (2nd𝑧))
99 csbeq1a 3078 . . . . . . . . . . . . . . . 16 (𝑘 = (2nd𝑧) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10098, 99syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10191, 92, 1003eqtrd 2224 . . . . . . . . . . . . . 14 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
102101expl 378 . . . . . . . . . . . . 13 (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10387, 89, 102exlimd 1607 . . . . . . . . . . . 12 (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10483, 86, 103exlimd 1607 . . . . . . . . . . 11 (𝜑 → (∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10582, 104biimtrid 152 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
106105imp 124 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
107106prodeq2dv 11588 . . . . . . . 8 (𝜑 → ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10861, 107eqtr4d 2223 . . . . . . 7 (𝜑 → ∏𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
10947, 108eqtrid 2232 . . . . . 6 (𝜑 → ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11043, 109eqtrd 2220 . . . . 5 (𝜑 → ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11112, 110eqtrid 2232 . . . 4 (𝜑 → ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
112111adantr 276 . . 3 ((𝜑𝜓) → ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
1133, 112oveq12d 5906 . 2 ((𝜑𝜓) → (∏𝑗𝑥𝑘𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶) = (∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
114 fprod2d.5 . . . . 5 (𝜑 → ¬ 𝑦𝑥)
115 disjsn 3666 . . . . 5 ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝑥)
116114, 115sylibr 134 . . . 4 (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
117 eqidd 2188 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
118 fprod2dlemstep.x . . . . 5 (𝜑𝑥 ∈ Fin)
11915a1i 9 . . . . 5 (𝜑𝑦 ∈ V)
120 unsnfi 6932 . . . . 5 ((𝑥 ∈ Fin ∧ 𝑦 ∈ V ∧ ¬ 𝑦𝑥) → (𝑥 ∪ {𝑦}) ∈ Fin)
121118, 119, 114, 120syl3anc 1248 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
12213sselda 3167 . . . . 5 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗𝐴)
12326anassrs 400 . . . . . 6 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
12418, 123fprodcl 11629 . . . . 5 ((𝜑𝑗𝐴) → ∏𝑘𝐵 𝐶 ∈ ℂ)
125122, 124syldan 282 . . . 4 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ∏𝑘𝐵 𝐶 ∈ ℂ)
126116, 117, 121, 125fprodsplit 11619 . . 3 (𝜑 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = (∏𝑗𝑥𝑘𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶))
127126adantr 276 . 2 ((𝜑𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = (∏𝑗𝑥𝑘𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶))
128 eliun 3902 . . . . . . . . . 10 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵))
129 xp1st 6180 . . . . . . . . . . . . . 14 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ {𝑗})
130 elsni 3622 . . . . . . . . . . . . . 14 ((1st𝑧) ∈ {𝑗} → (1st𝑧) = 𝑗)
131129, 130syl 14 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) = 𝑗)
132131eleq1d 2256 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑗} × 𝐵) → ((1st𝑧) ∈ 𝑥𝑗𝑥))
133132biimparc 299 . . . . . . . . . . 11 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → (1st𝑧) ∈ 𝑥)
134133rexlimiva 2599 . . . . . . . . . 10 (∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
135128, 134sylbi 121 . . . . . . . . 9 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
136 xp1st 6180 . . . . . . . . 9 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → (1st𝑧) ∈ {𝑦})
137135, 136anim12i 338 . . . . . . . 8 ((𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
138 elin 3330 . . . . . . . 8 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ↔ (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)))
139 elin 3330 . . . . . . . 8 ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
140137, 138, 1393imtr4i 201 . . . . . . 7 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → (1st𝑧) ∈ (𝑥 ∩ {𝑦}))
141116eleq2d 2257 . . . . . . . 8 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st𝑧) ∈ ∅))
142 noel 3438 . . . . . . . . 9 ¬ (1st𝑧) ∈ ∅
143142pm2.21i 647 . . . . . . . 8 ((1st𝑧) ∈ ∅ → 𝑧 ∈ ∅)
144141, 143biimtrdi 163 . . . . . . 7 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
145140, 144syl5 32 . . . . . 6 (𝜑 → (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝑧 ∈ ∅))
146145ssrdv 3173 . . . . 5 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅)
147 ss0 3475 . . . . 5 (( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅ → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
148146, 147syl 14 . . . 4 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
149 iunxun 3978 . . . . . 6 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
150 nfcv 2329 . . . . . . . . 9 𝑚({𝑗} × 𝐵)
151 nfcv 2329 . . . . . . . . . 10 𝑗{𝑚}
152151, 5nfxp 4665 . . . . . . . . 9 𝑗({𝑚} × 𝑚 / 𝑗𝐵)
153 sneq 3615 . . . . . . . . . 10 (𝑗 = 𝑚 → {𝑗} = {𝑚})
154153, 8xpeq12d 4663 . . . . . . . . 9 (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × 𝑚 / 𝑗𝐵))
155150, 152, 154cbviun 3935 . . . . . . . 8 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵)
156 sneq 3615 . . . . . . . . . 10 (𝑚 = 𝑦 → {𝑚} = {𝑦})
157156, 38xpeq12d 4663 . . . . . . . . 9 (𝑚 = 𝑦 → ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵))
15815, 157iunxsn 3975 . . . . . . . 8 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
159155, 158eqtri 2208 . . . . . . 7 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
160159uneq2i 3298 . . . . . 6 ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
161149, 160eqtri 2208 . . . . 5 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
162161a1i 9 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵)))
163 snfig 6828 . . . . . . . 8 (𝑗 ∈ V → {𝑗} ∈ Fin)
164163elv 2753 . . . . . . 7 {𝑗} ∈ Fin
165122, 18syldan 282 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
166 xpfi 6943 . . . . . . 7 (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
167164, 165, 166sylancr 414 . . . . . 6 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
168167ralrimiva 2560 . . . . 5 (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
169 disjsnxp 6252 . . . . . 6 Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)
170169a1i 9 . . . . 5 (𝜑Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵))
171 iunfidisj 6959 . . . . 5 (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin ∧ Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
172121, 168, 170, 171syl3anc 1248 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
173 eliun 3902 . . . . . 6 (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
174 elxp 4655 . . . . . . . 8 (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)))
175 simprl 529 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
176 simprrl 539 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 ∈ {𝑗})
177 elsni 3622 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
178176, 177syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 = 𝑗)
179178opeq1d 3796 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
180175, 179eqtrd 2220 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
181180, 90syl 14 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 = 𝐶)
182 simpll 527 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝜑)
183122adantr 276 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑗𝐴)
184 simprrr 540 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑘𝐵)
185182, 183, 184, 26syl12anc 1246 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐶 ∈ ℂ)
186181, 185eqeltrd 2264 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 ∈ ℂ)
187186ex 115 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
188187exlimdvv 1907 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
189174, 188biimtrid 152 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
190189rexlimdva 2604 . . . . . 6 (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
191173, 190biimtrid 152 . . . . 5 (𝜑 → (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
192191imp 124 . . . 4 ((𝜑𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
193148, 162, 172, 192fprodsplit 11619 . . 3 (𝜑 → ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
194193adantr 276 . 2 ((𝜑𝜓) → ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
195113, 127, 1943eqtr4d 2230 1 ((𝜑𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105   = wceq 1363  wex 1502  wcel 2158  wral 2465  wrex 2466  Vcvv 2749  csb 3069  cun 3139  cin 3140  wss 3141  c0 3434  {csn 3604  cop 3607   ciun 3898  Disj wdisj 3992   × cxp 4636  cres 4640  1-1-ontowf1o 5227  cfv 5228  (class class class)co 5888  1st c1st 6153  2nd c2nd 6154  Fincfn 6754  cc 7823   · cmul 7830  cprod 11572
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 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943  ax-arch 7944  ax-caucvg 7945
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 6155  df-2nd 6156  df-recs 6320  df-irdg 6385  df-frec 6406  df-1o 6431  df-oadd 6435  df-er 6549  df-en 6755  df-dom 6756  df-fin 6757  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-3 8993  df-4 8994  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fz 10023  df-fzo 10157  df-seqfrec 10460  df-exp 10534  df-ihash 10770  df-cj 10865  df-re 10866  df-im 10867  df-rsqrt 11021  df-abs 11022  df-clim 11301  df-proddc 11573
This theorem is referenced by:  fprod2d  11645
  Copyright terms: Public domain W3C validator