Metamath Proof Explorer

Theorem mulsproplem9

Description: Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 ⊢φ→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
mulsproplem9.1 ⊢φ→A∈No
mulsproplem9.2 ⊢φ→B∈No
Assertion mulsproplem9 ⊢φ→g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss≪si|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw

Proof

Step Hyp Ref Expression
1 mulsproplem.1 ⊢φ→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
2 mulsproplem9.1 ⊢φ→A∈No
3 mulsproplem9.2 ⊢φ→B∈No
4 eqid ⊢p∈L⁡A,q∈L⁡B⟼p⋅sB+sA⋅sq-sp⋅sq=p∈L⁡A,q∈L⁡B⟼p⋅sB+sA⋅sq-sp⋅sq
5 4 rnmpo ⊢ran⁡p∈L⁡A,q∈L⁡B⟼p⋅sB+sA⋅sq-sp⋅sq=g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq
6 fvex ⊢L⁡A∈V
7 fvex ⊢L⁡B∈V
8 6 7 mpoex ⊢p∈L⁡A,q∈L⁡B⟼p⋅sB+sA⋅sq-sp⋅sq∈V
9 8 rnex ⊢ran⁡p∈L⁡A,q∈L⁡B⟼p⋅sB+sA⋅sq-sp⋅sq∈V
10 5 9 eqeltrri ⊢g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∈V
11 eqid ⊢r∈R⁡A,s∈R⁡B⟼r⋅sB+sA⋅ss-sr⋅ss=r∈R⁡A,s∈R⁡B⟼r⋅sB+sA⋅ss-sr⋅ss
12 11 rnmpo ⊢ran⁡r∈R⁡A,s∈R⁡B⟼r⋅sB+sA⋅ss-sr⋅ss=h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss
13 fvex ⊢R⁡A∈V
14 fvex ⊢R⁡B∈V
15 13 14 mpoex ⊢r∈R⁡A,s∈R⁡B⟼r⋅sB+sA⋅ss-sr⋅ss∈V
16 15 rnex ⊢ran⁡r∈R⁡A,s∈R⁡B⟼r⋅sB+sA⋅ss-sr⋅ss∈V
17 12 16 eqeltrri ⊢h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∈V
18 10 17 unex ⊢g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∈V
19 18 a1i ⊢φ→g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∈V
20 eqid ⊢t∈L⁡A,u∈R⁡B⟼t⋅sB+sA⋅su-st⋅su=t∈L⁡A,u∈R⁡B⟼t⋅sB+sA⋅su-st⋅su
21 20 rnmpo ⊢ran⁡t∈L⁡A,u∈R⁡B⟼t⋅sB+sA⋅su-st⋅su=i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su
22 6 14 mpoex ⊢t∈L⁡A,u∈R⁡B⟼t⋅sB+sA⋅su-st⋅su∈V
23 22 rnex ⊢ran⁡t∈L⁡A,u∈R⁡B⟼t⋅sB+sA⋅su-st⋅su∈V
24 21 23 eqeltrri ⊢i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∈V
25 eqid ⊢v∈R⁡A,w∈L⁡B⟼v⋅sB+sA⋅sw-sv⋅sw=v∈R⁡A,w∈L⁡B⟼v⋅sB+sA⋅sw-sv⋅sw
26 25 rnmpo ⊢ran⁡v∈R⁡A,w∈L⁡B⟼v⋅sB+sA⋅sw-sv⋅sw=j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw
27 13 7 mpoex ⊢v∈R⁡A,w∈L⁡B⟼v⋅sB+sA⋅sw-sv⋅sw∈V
28 27 rnex ⊢ran⁡v∈R⁡A,w∈L⁡B⟼v⋅sB+sA⋅sw-sv⋅sw∈V
29 26 28 eqeltrri ⊢j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw∈V
30 24 29 unex ⊢i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw∈V
31 30 a1i ⊢φ→i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw∈V
32 1 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
33 leftssold ⊢L⁡A⊆Old⁡bday⁡A
34 simprl ⊢φ∧p∈L⁡A∧q∈L⁡B→p∈L⁡A
35 33 34 sselid ⊢φ∧p∈L⁡A∧q∈L⁡B→p∈Old⁡bday⁡A
36 3 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B→B∈No
37 32 35 36 mulsproplem2 ⊢φ∧p∈L⁡A∧q∈L⁡B→p⋅sB∈No
38 2 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B→A∈No
39 leftssold ⊢L⁡B⊆Old⁡bday⁡B
40 simprr ⊢φ∧p∈L⁡A∧q∈L⁡B→q∈L⁡B
41 39 40 sselid ⊢φ∧p∈L⁡A∧q∈L⁡B→q∈Old⁡bday⁡B
42 32 38 41 mulsproplem3 ⊢φ∧p∈L⁡A∧q∈L⁡B→A⋅sq∈No
43 37 42 addscld ⊢φ∧p∈L⁡A∧q∈L⁡B→p⋅sB+sA⋅sq∈No
44 32 35 41 mulsproplem4 ⊢φ∧p∈L⁡A∧q∈L⁡B→p⋅sq∈No
45 43 44 subscld ⊢φ∧p∈L⁡A∧q∈L⁡B→p⋅sB+sA⋅sq-sp⋅sq∈No
46 eleq1 ⊢g=p⋅sB+sA⋅sq-sp⋅sq→g∈No↔p⋅sB+sA⋅sq-sp⋅sq∈No
47 45 46 syl5ibrcom ⊢φ∧p∈L⁡A∧q∈L⁡B→g=p⋅sB+sA⋅sq-sp⋅sq→g∈No
48 47 rexlimdvva ⊢φ→∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq→g∈No
49 48 abssdv ⊢φ→g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq⊆No
50 1 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
51 rightssold ⊢R⁡A⊆Old⁡bday⁡A
52 simprl ⊢φ∧r∈R⁡A∧s∈R⁡B→r∈R⁡A
53 51 52 sselid ⊢φ∧r∈R⁡A∧s∈R⁡B→r∈Old⁡bday⁡A
54 3 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B→B∈No
55 50 53 54 mulsproplem2 ⊢φ∧r∈R⁡A∧s∈R⁡B→r⋅sB∈No
56 2 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B→A∈No
57 rightssold ⊢R⁡B⊆Old⁡bday⁡B
58 simprr ⊢φ∧r∈R⁡A∧s∈R⁡B→s∈R⁡B
59 57 58 sselid ⊢φ∧r∈R⁡A∧s∈R⁡B→s∈Old⁡bday⁡B
60 50 56 59 mulsproplem3 ⊢φ∧r∈R⁡A∧s∈R⁡B→A⋅ss∈No
61 55 60 addscld ⊢φ∧r∈R⁡A∧s∈R⁡B→r⋅sB+sA⋅ss∈No
62 50 53 59 mulsproplem4 ⊢φ∧r∈R⁡A∧s∈R⁡B→r⋅ss∈No
63 61 62 subscld ⊢φ∧r∈R⁡A∧s∈R⁡B→r⋅sB+sA⋅ss-sr⋅ss∈No
64 eleq1 ⊢h=r⋅sB+sA⋅ss-sr⋅ss→h∈No↔r⋅sB+sA⋅ss-sr⋅ss∈No
65 63 64 syl5ibrcom ⊢φ∧r∈R⁡A∧s∈R⁡B→h=r⋅sB+sA⋅ss-sr⋅ss→h∈No
66 65 rexlimdvva ⊢φ→∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss→h∈No
67 66 abssdv ⊢φ→h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss⊆No
68 49 67 unssd ⊢φ→g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss⊆No
69 1 adantr ⊢φ∧t∈L⁡A∧u∈R⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
70 simprl ⊢φ∧t∈L⁡A∧u∈R⁡B→t∈L⁡A
71 33 70 sselid ⊢φ∧t∈L⁡A∧u∈R⁡B→t∈Old⁡bday⁡A
72 3 adantr ⊢φ∧t∈L⁡A∧u∈R⁡B→B∈No
73 69 71 72 mulsproplem2 ⊢φ∧t∈L⁡A∧u∈R⁡B→t⋅sB∈No
74 2 adantr ⊢φ∧t∈L⁡A∧u∈R⁡B→A∈No
75 simprr ⊢φ∧t∈L⁡A∧u∈R⁡B→u∈R⁡B
76 57 75 sselid ⊢φ∧t∈L⁡A∧u∈R⁡B→u∈Old⁡bday⁡B
77 69 74 76 mulsproplem3 ⊢φ∧t∈L⁡A∧u∈R⁡B→A⋅su∈No
78 73 77 addscld ⊢φ∧t∈L⁡A∧u∈R⁡B→t⋅sB+sA⋅su∈No
79 69 71 76 mulsproplem4 ⊢φ∧t∈L⁡A∧u∈R⁡B→t⋅su∈No
80 78 79 subscld ⊢φ∧t∈L⁡A∧u∈R⁡B→t⋅sB+sA⋅su-st⋅su∈No
81 eleq1 ⊢i=t⋅sB+sA⋅su-st⋅su→i∈No↔t⋅sB+sA⋅su-st⋅su∈No
82 80 81 syl5ibrcom ⊢φ∧t∈L⁡A∧u∈R⁡B→i=t⋅sB+sA⋅su-st⋅su→i∈No
83 82 rexlimdvva ⊢φ→∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su→i∈No
84 83 abssdv ⊢φ→i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su⊆No
85 1 adantr ⊢φ∧v∈R⁡A∧w∈L⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
86 simprl ⊢φ∧v∈R⁡A∧w∈L⁡B→v∈R⁡A
87 51 86 sselid ⊢φ∧v∈R⁡A∧w∈L⁡B→v∈Old⁡bday⁡A
88 3 adantr ⊢φ∧v∈R⁡A∧w∈L⁡B→B∈No
89 85 87 88 mulsproplem2 ⊢φ∧v∈R⁡A∧w∈L⁡B→v⋅sB∈No
90 2 adantr ⊢φ∧v∈R⁡A∧w∈L⁡B→A∈No
91 simprr ⊢φ∧v∈R⁡A∧w∈L⁡B→w∈L⁡B
92 39 91 sselid ⊢φ∧v∈R⁡A∧w∈L⁡B→w∈Old⁡bday⁡B
93 85 90 92 mulsproplem3 ⊢φ∧v∈R⁡A∧w∈L⁡B→A⋅sw∈No
94 89 93 addscld ⊢φ∧v∈R⁡A∧w∈L⁡B→v⋅sB+sA⋅sw∈No
95 85 87 92 mulsproplem4 ⊢φ∧v∈R⁡A∧w∈L⁡B→v⋅sw∈No
96 94 95 subscld ⊢φ∧v∈R⁡A∧w∈L⁡B→v⋅sB+sA⋅sw-sv⋅sw∈No
97 eleq1 ⊢j=v⋅sB+sA⋅sw-sv⋅sw→j∈No↔v⋅sB+sA⋅sw-sv⋅sw∈No
98 96 97 syl5ibrcom ⊢φ∧v∈R⁡A∧w∈L⁡B→j=v⋅sB+sA⋅sw-sv⋅sw→j∈No
99 98 rexlimdvva ⊢φ→∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw→j∈No
100 99 abssdv ⊢φ→j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw⊆No
101 84 100 unssd ⊢φ→i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw⊆No
102 elun ⊢x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss↔x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∨x∈h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss
103 vex ⊢x∈V
104 eqeq1 ⊢g=x→g=p⋅sB+sA⋅sq-sp⋅sq↔x=p⋅sB+sA⋅sq-sp⋅sq
105 104 2rexbidv ⊢g=x→∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq
106 103 105 elab ⊢x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq
107 eqeq1 ⊢h=x→h=r⋅sB+sA⋅ss-sr⋅ss↔x=r⋅sB+sA⋅ss-sr⋅ss
108 107 2rexbidv ⊢h=x→∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss↔∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss
109 103 108 elab ⊢x∈h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss↔∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss
110 106 109 orbi12i ⊢x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∨x∈h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss
111 102 110 bitri ⊢x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss
112 elun ⊢y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∨y∈j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw
113 vex ⊢y∈V
114 eqeq1 ⊢i=y→i=t⋅sB+sA⋅su-st⋅su↔y=t⋅sB+sA⋅su-st⋅su
115 114 2rexbidv ⊢i=y→∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su↔∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su
116 113 115 elab ⊢y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su↔∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su
117 eqeq1 ⊢j=y→j=v⋅sB+sA⋅sw-sv⋅sw↔y=v⋅sB+sA⋅sw-sv⋅sw
118 117 2rexbidv ⊢j=y→∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
119 113 118 elab ⊢y∈j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
120 116 119 orbi12i ⊢y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∨y∈j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
121 112 120 bitri ⊢y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
122 111 121 anbi12i ⊢x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∧y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
123 anddi ⊢∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
124 122 123 bitri ⊢x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∧y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw↔∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw
125 1 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
126 2 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→A∈No
127 3 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→B∈No
128 simprll ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→p∈L⁡A
129 simprlr ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→q∈L⁡B
130 simprrl ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→t∈L⁡A
131 simprrr ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→u∈R⁡B
132 125 126 127 128 129 130 131 mulsproplem5 ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→p⋅sB+sA⋅sq-sp⋅sq<st⋅sB+sA⋅su-st⋅su
133 breq2 ⊢y=t⋅sB+sA⋅su-st⋅su→p⋅sB+sA⋅sq-sp⋅sq<sy↔p⋅sB+sA⋅sq-sp⋅sq<st⋅sB+sA⋅su-st⋅su
134 132 133 syl5ibrcom ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→y=t⋅sB+sA⋅su-st⋅su→p⋅sB+sA⋅sq-sp⋅sq<sy
135 134 anassrs ⊢φ∧p∈L⁡A∧q∈L⁡B∧t∈L⁡A∧u∈R⁡B→y=t⋅sB+sA⋅su-st⋅su→p⋅sB+sA⋅sq-sp⋅sq<sy
136 135 rexlimdvva ⊢φ∧p∈L⁡A∧q∈L⁡B→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→p⋅sB+sA⋅sq-sp⋅sq<sy
137 breq1 ⊢x=p⋅sB+sA⋅sq-sp⋅sq→x<sy↔p⋅sB+sA⋅sq-sp⋅sq<sy
138 137 imbi2d ⊢x=p⋅sB+sA⋅sq-sp⋅sq→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy↔∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→p⋅sB+sA⋅sq-sp⋅sq<sy
139 136 138 syl5ibrcom ⊢φ∧p∈L⁡A∧q∈L⁡B→x=p⋅sB+sA⋅sq-sp⋅sq→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy
140 139 rexlimdvva ⊢φ→∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy
141 140 impd ⊢φ→∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy
142 1 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
143 2 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→A∈No
144 3 adantr ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→B∈No
145 simprll ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→p∈L⁡A
146 simprlr ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→q∈L⁡B
147 simprrl ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→v∈R⁡A
148 simprrr ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→w∈L⁡B
149 142 143 144 145 146 147 148 mulsproplem6 ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→p⋅sB+sA⋅sq-sp⋅sq<sv⋅sB+sA⋅sw-sv⋅sw
150 breq2 ⊢y=v⋅sB+sA⋅sw-sv⋅sw→p⋅sB+sA⋅sq-sp⋅sq<sy↔p⋅sB+sA⋅sq-sp⋅sq<sv⋅sB+sA⋅sw-sv⋅sw
151 149 150 syl5ibrcom ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→y=v⋅sB+sA⋅sw-sv⋅sw→p⋅sB+sA⋅sq-sp⋅sq<sy
152 151 anassrs ⊢φ∧p∈L⁡A∧q∈L⁡B∧v∈R⁡A∧w∈L⁡B→y=v⋅sB+sA⋅sw-sv⋅sw→p⋅sB+sA⋅sq-sp⋅sq<sy
153 152 rexlimdvva ⊢φ∧p∈L⁡A∧q∈L⁡B→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→p⋅sB+sA⋅sq-sp⋅sq<sy
154 137 imbi2d ⊢x=p⋅sB+sA⋅sq-sp⋅sq→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy↔∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→p⋅sB+sA⋅sq-sp⋅sq<sy
155 153 154 syl5ibrcom ⊢φ∧p∈L⁡A∧q∈L⁡B→x=p⋅sB+sA⋅sq-sp⋅sq→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
156 155 rexlimdvva ⊢φ→∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
157 156 impd ⊢φ→∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
158 141 157 jaod ⊢φ→∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
159 1 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
160 2 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→A∈No
161 3 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→B∈No
162 simprll ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→r∈R⁡A
163 simprlr ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→s∈R⁡B
164 simprrl ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→t∈L⁡A
165 simprrr ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→u∈R⁡B
166 159 160 161 162 163 164 165 mulsproplem7 ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→r⋅sB+sA⋅ss-sr⋅ss<st⋅sB+sA⋅su-st⋅su
167 breq2 ⊢y=t⋅sB+sA⋅su-st⋅su→r⋅sB+sA⋅ss-sr⋅ss<sy↔r⋅sB+sA⋅ss-sr⋅ss<st⋅sB+sA⋅su-st⋅su
168 166 167 syl5ibrcom ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→y=t⋅sB+sA⋅su-st⋅su→r⋅sB+sA⋅ss-sr⋅ss<sy
169 168 anassrs ⊢φ∧r∈R⁡A∧s∈R⁡B∧t∈L⁡A∧u∈R⁡B→y=t⋅sB+sA⋅su-st⋅su→r⋅sB+sA⋅ss-sr⋅ss<sy
170 169 rexlimdvva ⊢φ∧r∈R⁡A∧s∈R⁡B→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→r⋅sB+sA⋅ss-sr⋅ss<sy
171 breq1 ⊢x=r⋅sB+sA⋅ss-sr⋅ss→x<sy↔r⋅sB+sA⋅ss-sr⋅ss<sy
172 171 imbi2d ⊢x=r⋅sB+sA⋅ss-sr⋅ss→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy↔∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→r⋅sB+sA⋅ss-sr⋅ss<sy
173 170 172 syl5ibrcom ⊢φ∧r∈R⁡A∧s∈R⁡B→x=r⋅sB+sA⋅ss-sr⋅ss→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy
174 173 rexlimdvva ⊢φ→∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss→∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy
175 174 impd ⊢φ→∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su→x<sy
176 1 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→∀a∈No∀b∈No∀c∈No∀d∈No∀e∈No∀f∈Nobday⁡a+bday⁡b∪bday⁡c+bday⁡e∪bday⁡d+bday⁡f∪bday⁡c+bday⁡f∪bday⁡d+bday⁡e∈bday⁡A+bday⁡B∪bday⁡C+bday⁡E∪bday⁡D+bday⁡F∪bday⁡C+bday⁡F∪bday⁡D+bday⁡E→a⋅sb∈No∧c<sd∧e<sf→c⋅sf-sc⋅se<sd⋅sf-sd⋅se
177 2 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→A∈No
178 3 adantr ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→B∈No
179 simprll ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→r∈R⁡A
180 simprlr ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→s∈R⁡B
181 simprrl ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→v∈R⁡A
182 simprrr ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→w∈L⁡B
183 176 177 178 179 180 181 182 mulsproplem8 ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→r⋅sB+sA⋅ss-sr⋅ss<sv⋅sB+sA⋅sw-sv⋅sw
184 breq2 ⊢y=v⋅sB+sA⋅sw-sv⋅sw→r⋅sB+sA⋅ss-sr⋅ss<sy↔r⋅sB+sA⋅ss-sr⋅ss<sv⋅sB+sA⋅sw-sv⋅sw
185 183 184 syl5ibrcom ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→y=v⋅sB+sA⋅sw-sv⋅sw→r⋅sB+sA⋅ss-sr⋅ss<sy
186 185 anassrs ⊢φ∧r∈R⁡A∧s∈R⁡B∧v∈R⁡A∧w∈L⁡B→y=v⋅sB+sA⋅sw-sv⋅sw→r⋅sB+sA⋅ss-sr⋅ss<sy
187 186 rexlimdvva ⊢φ∧r∈R⁡A∧s∈R⁡B→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→r⋅sB+sA⋅ss-sr⋅ss<sy
188 171 imbi2d ⊢x=r⋅sB+sA⋅ss-sr⋅ss→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy↔∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→r⋅sB+sA⋅ss-sr⋅ss<sy
189 187 188 syl5ibrcom ⊢φ∧r∈R⁡A∧s∈R⁡B→x=r⋅sB+sA⋅ss-sr⋅ss→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
190 189 rexlimdvva ⊢φ→∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss→∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
191 190 impd ⊢φ→∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
192 175 191 jaod ⊢φ→∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
193 158 192 jaod ⊢φ→∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃p∈L⁡A∃q∈L⁡Bx=p⋅sB+sA⋅sq-sp⋅sq∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃t∈L⁡A∃u∈R⁡By=t⋅sB+sA⋅su-st⋅su∨∃r∈R⁡A∃s∈R⁡Bx=r⋅sB+sA⋅ss-sr⋅ss∧∃v∈R⁡A∃w∈L⁡By=v⋅sB+sA⋅sw-sv⋅sw→x<sy
194 124 193 biimtrid ⊢φ→x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∧y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw→x<sy
195 194 3impib ⊢φ∧x∈g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss∧y∈i|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw→x<sy
196 19 31 68 101 195 ssltd ⊢φ→g|∃p∈L⁡A∃q∈L⁡Bg=p⋅sB+sA⋅sq-sp⋅sq∪h|∃r∈R⁡A∃s∈R⁡Bh=r⋅sB+sA⋅ss-sr⋅ss≪si|∃t∈L⁡A∃u∈R⁡Bi=t⋅sB+sA⋅su-st⋅su∪j|∃v∈R⁡A∃w∈L⁡Bj=v⋅sB+sA⋅sw-sv⋅sw