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

Theorem fprod2dlemstep 11585
Description: Lemma for fprod2d 11586- 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 109 . . . 4 ((𝜑𝜓) → 𝜓)
2 fprod2d.7 . . . 4 (𝜓 ↔ ∏𝑗𝑥𝑘𝐵 𝐶 = ∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
31, 2sylib 121 . . 3 ((𝜑𝜓) → ∏𝑗𝑥𝑘𝐵 𝐶 = ∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
4 nfcv 2312 . . . . . 6 𝑚𝑘𝐵 𝐶
5 nfcsb1v 3082 . . . . . . 7 𝑗𝑚 / 𝑗𝐵
6 nfcsb1v 3082 . . . . . . 7 𝑗𝑚 / 𝑗𝐶
75, 6nfcprod 11518 . . . . . 6 𝑗𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
8 csbeq1a 3058 . . . . . . 7 (𝑗 = 𝑚𝐵 = 𝑚 / 𝑗𝐵)
9 csbeq1a 3058 . . . . . . . 8 (𝑗 = 𝑚𝐶 = 𝑚 / 𝑗𝐶)
109adantr 274 . . . . . . 7 ((𝑗 = 𝑚𝑘𝐵) → 𝐶 = 𝑚 / 𝑗𝐶)
118, 10prodeq12dv 11532 . . . . . 6 (𝑗 = 𝑚 → ∏𝑘𝐵 𝐶 = ∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶)
124, 7, 11cbvprodi 11523 . . . . 5 𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶 = ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
13 fprod2d.6 . . . . . . . . 9 (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
1413unssbd 3305 . . . . . . . 8 (𝜑 → {𝑦} ⊆ 𝐴)
15 vex 2733 . . . . . . . . 9 𝑦 ∈ V
1615snss 3709 . . . . . . . 8 (𝑦𝐴 ↔ {𝑦} ⊆ 𝐴)
1714, 16sylibr 133 . . . . . . 7 (𝜑𝑦𝐴)
18 fprod2d.3 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
1918ralrimiva 2543 . . . . . . . . 9 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
20 nfcsb1v 3082 . . . . . . . . . . 11 𝑗𝑦 / 𝑗𝐵
2120nfel1 2323 . . . . . . . . . 10 𝑗𝑦 / 𝑗𝐵 ∈ Fin
22 csbeq1a 3058 . . . . . . . . . . 11 (𝑗 = 𝑦𝐵 = 𝑦 / 𝑗𝐵)
2322eleq1d 2239 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ 𝑦 / 𝑗𝐵 ∈ Fin))
2421, 23rspc 2828 . . . . . . . . 9 (𝑦𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑦 / 𝑗𝐵 ∈ Fin))
2517, 19, 24sylc 62 . . . . . . . 8 (𝜑𝑦 / 𝑗𝐵 ∈ Fin)
26 fprod2d.4 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
2726ralrimivva 2552 . . . . . . . . . 10 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ)
28 nfcsb1v 3082 . . . . . . . . . . . . 13 𝑗𝑦 / 𝑗𝐶
2928nfel1 2323 . . . . . . . . . . . 12 𝑗𝑦 / 𝑗𝐶 ∈ ℂ
3020, 29nfralw 2507 . . . . . . . . . . 11 𝑗𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ
31 csbeq1a 3058 . . . . . . . . . . . . 13 (𝑗 = 𝑦𝐶 = 𝑦 / 𝑗𝐶)
3231eleq1d 2239 . . . . . . . . . . . 12 (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ 𝑦 / 𝑗𝐶 ∈ ℂ))
3322, 32raleqbidv 2677 . . . . . . . . . . 11 (𝑗 = 𝑦 → (∀𝑘𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3430, 33rspc 2828 . . . . . . . . . 10 (𝑦𝐴 → (∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3517, 27, 34sylc 62 . . . . . . . . 9 (𝜑 → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
3635r19.21bi 2558 . . . . . . . 8 ((𝜑𝑘𝑦 / 𝑗𝐵) → 𝑦 / 𝑗𝐶 ∈ ℂ)
3725, 36fprodcl 11570 . . . . . . 7 (𝜑 → ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
38 csbeq1 3052 . . . . . . . . 9 (𝑚 = 𝑦𝑚 / 𝑗𝐵 = 𝑦 / 𝑗𝐵)
39 csbeq1 3052 . . . . . . . . . 10 (𝑚 = 𝑦𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4039adantr 274 . . . . . . . . 9 ((𝑚 = 𝑦𝑘𝑚 / 𝑗𝐵) → 𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4138, 40prodeq12dv 11532 . . . . . . . 8 (𝑚 = 𝑦 → ∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4241prodsn 11556 . . . . . . 7 ((𝑦𝐴 ∧ ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ) → ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4317, 37, 42syl2anc 409 . . . . . 6 (𝜑 → ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
44 nfcv 2312 . . . . . . . 8 𝑚𝑦 / 𝑗𝐶
45 nfcsb1v 3082 . . . . . . . 8 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶
46 csbeq1a 3058 . . . . . . . 8 (𝑘 = 𝑚𝑦 / 𝑗𝐶 = 𝑚 / 𝑘𝑦 / 𝑗𝐶)
4744, 45, 46cbvprodi 11523 . . . . . . 7 𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = ∏𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶
48 csbeq1 3052 . . . . . . . . 9 (𝑚 = (2nd𝑧) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
49 snfig 6792 . . . . . . . . . . 11 (𝑦 ∈ V → {𝑦} ∈ Fin)
5049elv 2734 . . . . . . . . . 10 {𝑦} ∈ Fin
51 xpfi 6907 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑗𝐵 ∈ Fin) → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
5250, 25, 51sylancr 412 . . . . . . . . 9 (𝜑 → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
53 2ndconst 6201 . . . . . . . . . 10 (𝑦𝐴 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
5417, 53syl 14 . . . . . . . . 9 (𝜑 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
55 fvres 5520 . . . . . . . . . 10 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5655adantl 275 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5745nfel1 2323 . . . . . . . . . . 11 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ
5846eleq1d 2239 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝑦 / 𝑗𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
5957, 58rspc 2828 . . . . . . . . . 10 (𝑚𝑦 / 𝑗𝐵 → (∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
6035, 59mpan9 279 . . . . . . . . 9 ((𝜑𝑚𝑦 / 𝑗𝐵) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ)
6148, 52, 54, 56, 60fprodf1o 11551 . . . . . . . 8 (𝜑 → ∏𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
62 elxp 4628 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)))
63 nfv 1521 . . . . . . . . . . . . . . 15 𝑗 𝑧 = ⟨𝑚, 𝑘
64 nfv 1521 . . . . . . . . . . . . . . . 16 𝑗 𝑚 ∈ {𝑦}
6520nfcri 2306 . . . . . . . . . . . . . . . 16 𝑗 𝑘𝑦 / 𝑗𝐵
6664, 65nfan 1558 . . . . . . . . . . . . . . 15 𝑗(𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)
6763, 66nfan 1558 . . . . . . . . . . . . . 14 𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
6867nfex 1630 . . . . . . . . . . . . 13 𝑗𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
69 nfv 1521 . . . . . . . . . . . . 13 𝑚𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))
70 opeq1 3765 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
7170eqeq2d 2182 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
72 eleq1w 2231 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑗 → (𝑚 ∈ {𝑦} ↔ 𝑗 ∈ {𝑦}))
73 velsn 3600 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
7472, 73bitrdi 195 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → (𝑚 ∈ {𝑦} ↔ 𝑗 = 𝑦))
7574anbi1d 462 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑗 = 𝑦𝑘𝑦 / 𝑗𝐵)))
7622eleq2d 2240 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑦 → (𝑘𝐵𝑘𝑦 / 𝑗𝐵))
7776pm5.32i 451 . . . . . . . . . . . . . . . 16 ((𝑗 = 𝑦𝑘𝐵) ↔ (𝑗 = 𝑦𝑘𝑦 / 𝑗𝐵))
7875, 77bitr4di 197 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑗 = 𝑦𝑘𝐵)))
7971, 78anbi12d 470 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8079exbidv 1818 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8168, 69, 80cbvexv1 1745 . . . . . . . . . . . 12 (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
8262, 81bitri 183 . . . . . . . . . . 11 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
83 nfv 1521 . . . . . . . . . . . 12 𝑗𝜑
84 nfcv 2312 . . . . . . . . . . . . . 14 𝑗(2nd𝑧)
8584, 28nfcsbw 3085 . . . . . . . . . . . . 13 𝑗(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
8685nfeq2 2324 . . . . . . . . . . . 12 𝑗 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
87 nfv 1521 . . . . . . . . . . . . 13 𝑘𝜑
88 nfcsb1v 3082 . . . . . . . . . . . . . 14 𝑘(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
8988nfeq2 2324 . . . . . . . . . . . . 13 𝑘 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
90 fprod2d.1 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
9190ad2antlr 486 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = 𝐶)
9231ad2antrl 487 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐶 = 𝑦 / 𝑗𝐶)
93 fveq2 5496 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
94 vex 2733 . . . . . . . . . . . . . . . . . . 19 𝑗 ∈ V
95 vex 2733 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
9694, 95op2nd 6126 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
9793, 96eqtr2di 2220 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd𝑧))
9897ad2antlr 486 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑘 = (2nd𝑧))
99 csbeq1a 3058 . . . . . . . . . . . . . . . 16 (𝑘 = (2nd𝑧) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10098, 99syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10191, 92, 1003eqtrd 2207 . . . . . . . . . . . . . 14 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
102101expl 376 . . . . . . . . . . . . 13 (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10387, 89, 102exlimd 1590 . . . . . . . . . . . 12 (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10483, 86, 103exlimd 1590 . . . . . . . . . . 11 (𝜑 → (∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10582, 104syl5bi 151 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
106105imp 123 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
107106prodeq2dv 11529 . . . . . . . 8 (𝜑 → ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10861, 107eqtr4d 2206 . . . . . . 7 (𝜑 → ∏𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
10947, 108eqtrid 2215 . . . . . 6 (𝜑 → ∏𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11043, 109eqtrd 2203 . . . . 5 (𝜑 → ∏𝑚 ∈ {𝑦}∏𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11112, 110eqtrid 2215 . . . 4 (𝜑 → ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
112111adantr 274 . . 3 ((𝜑𝜓) → ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶 = ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
1133, 112oveq12d 5871 . 2 ((𝜑𝜓) → (∏𝑗𝑥𝑘𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶) = (∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
114 fprod2d.5 . . . . 5 (𝜑 → ¬ 𝑦𝑥)
115 disjsn 3645 . . . . 5 ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝑥)
116114, 115sylibr 133 . . . 4 (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
117 eqidd 2171 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
118 fprod2dlemstep.x . . . . 5 (𝜑𝑥 ∈ Fin)
11915a1i 9 . . . . 5 (𝜑𝑦 ∈ V)
120 unsnfi 6896 . . . . 5 ((𝑥 ∈ Fin ∧ 𝑦 ∈ V ∧ ¬ 𝑦𝑥) → (𝑥 ∪ {𝑦}) ∈ Fin)
121118, 119, 114, 120syl3anc 1233 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
12213sselda 3147 . . . . 5 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗𝐴)
12326anassrs 398 . . . . . 6 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
12418, 123fprodcl 11570 . . . . 5 ((𝜑𝑗𝐴) → ∏𝑘𝐵 𝐶 ∈ ℂ)
125122, 124syldan 280 . . . 4 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ∏𝑘𝐵 𝐶 ∈ ℂ)
126116, 117, 121, 125fprodsplit 11560 . . 3 (𝜑 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = (∏𝑗𝑥𝑘𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶))
127126adantr 274 . 2 ((𝜑𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = (∏𝑗𝑥𝑘𝐵 𝐶 · ∏𝑗 ∈ {𝑦}∏𝑘𝐵 𝐶))
128 eliun 3877 . . . . . . . . . 10 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵))
129 xp1st 6144 . . . . . . . . . . . . . 14 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ {𝑗})
130 elsni 3601 . . . . . . . . . . . . . 14 ((1st𝑧) ∈ {𝑗} → (1st𝑧) = 𝑗)
131129, 130syl 14 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) = 𝑗)
132131eleq1d 2239 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑗} × 𝐵) → ((1st𝑧) ∈ 𝑥𝑗𝑥))
133132biimparc 297 . . . . . . . . . . 11 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → (1st𝑧) ∈ 𝑥)
134133rexlimiva 2582 . . . . . . . . . 10 (∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
135128, 134sylbi 120 . . . . . . . . 9 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
136 xp1st 6144 . . . . . . . . 9 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → (1st𝑧) ∈ {𝑦})
137135, 136anim12i 336 . . . . . . . 8 ((𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
138 elin 3310 . . . . . . . 8 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ↔ (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)))
139 elin 3310 . . . . . . . 8 ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
140137, 138, 1393imtr4i 200 . . . . . . 7 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → (1st𝑧) ∈ (𝑥 ∩ {𝑦}))
141116eleq2d 2240 . . . . . . . 8 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st𝑧) ∈ ∅))
142 noel 3418 . . . . . . . . 9 ¬ (1st𝑧) ∈ ∅
143142pm2.21i 641 . . . . . . . 8 ((1st𝑧) ∈ ∅ → 𝑧 ∈ ∅)
144141, 143syl6bi 162 . . . . . . 7 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
145140, 144syl5 32 . . . . . 6 (𝜑 → (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝑧 ∈ ∅))
146145ssrdv 3153 . . . . 5 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅)
147 ss0 3455 . . . . 5 (( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅ → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
148146, 147syl 14 . . . 4 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
149 iunxun 3952 . . . . . 6 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
150 nfcv 2312 . . . . . . . . 9 𝑚({𝑗} × 𝐵)
151 nfcv 2312 . . . . . . . . . 10 𝑗{𝑚}
152151, 5nfxp 4638 . . . . . . . . 9 𝑗({𝑚} × 𝑚 / 𝑗𝐵)
153 sneq 3594 . . . . . . . . . 10 (𝑗 = 𝑚 → {𝑗} = {𝑚})
154153, 8xpeq12d 4636 . . . . . . . . 9 (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × 𝑚 / 𝑗𝐵))
155150, 152, 154cbviun 3910 . . . . . . . 8 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵)
156 sneq 3594 . . . . . . . . . 10 (𝑚 = 𝑦 → {𝑚} = {𝑦})
157156, 38xpeq12d 4636 . . . . . . . . 9 (𝑚 = 𝑦 → ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵))
15815, 157iunxsn 3949 . . . . . . . 8 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
159155, 158eqtri 2191 . . . . . . 7 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
160159uneq2i 3278 . . . . . 6 ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
161149, 160eqtri 2191 . . . . 5 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
162161a1i 9 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵)))
163 snfig 6792 . . . . . . . 8 (𝑗 ∈ V → {𝑗} ∈ Fin)
164163elv 2734 . . . . . . 7 {𝑗} ∈ Fin
165122, 18syldan 280 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
166 xpfi 6907 . . . . . . 7 (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
167164, 165, 166sylancr 412 . . . . . 6 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
168167ralrimiva 2543 . . . . 5 (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
169 disjsnxp 6216 . . . . . 6 Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)
170169a1i 9 . . . . 5 (𝜑Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵))
171 iunfidisj 6923 . . . . 5 (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin ∧ Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
172121, 168, 170, 171syl3anc 1233 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
173 eliun 3877 . . . . . 6 (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
174 elxp 4628 . . . . . . . 8 (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)))
175 simprl 526 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
176 simprrl 534 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 ∈ {𝑗})
177 elsni 3601 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
178176, 177syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 = 𝑗)
179178opeq1d 3771 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
180175, 179eqtrd 2203 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
181180, 90syl 14 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 = 𝐶)
182 simpll 524 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝜑)
183122adantr 274 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑗𝐴)
184 simprrr 535 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑘𝐵)
185182, 183, 184, 26syl12anc 1231 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐶 ∈ ℂ)
186181, 185eqeltrd 2247 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 ∈ ℂ)
187186ex 114 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
188187exlimdvv 1890 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
189174, 188syl5bi 151 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
190189rexlimdva 2587 . . . . . 6 (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
191173, 190syl5bi 151 . . . . 5 (𝜑 → (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
192191imp 123 . . . 4 ((𝜑𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
193148, 162, 172, 192fprodsplit 11560 . . 3 (𝜑 → ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
194193adantr 274 . 2 ((𝜑𝜓) → ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (∏𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 · ∏𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
195113, 127, 1943eqtr4d 2213 1 ((𝜑𝜓) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘𝐵 𝐶 = ∏𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104   = wceq 1348  wex 1485  wcel 2141  wral 2448  wrex 2449  Vcvv 2730  csb 3049  cun 3119  cin 3120  wss 3121  c0 3414  {csn 3583  cop 3586   ciun 3873  Disj wdisj 3966   × cxp 4609  cres 4613  1-1-ontowf1o 5197  cfv 5198  (class class class)co 5853  1st c1st 6117  2nd c2nd 6118  Fincfn 6718  cc 7772   · cmul 7779  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:  fprod2d  11586
  Copyright terms: Public domain W3C validator