Metamath Proof Explorer

Theorem sltmuls2

Description: One surreal set less-than relationship for cuts of A and B . (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses sltmuls2.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
sltmuls2.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
sltmuls2.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
sltmuls2.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
Assertion sltmuls2 ( 𝜑 → { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) )

Proof

Step Hyp Ref Expression
1 sltmuls2.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2 sltmuls2.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3 sltmuls2.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
4 sltmuls2.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
5 snex ⊢ { ( 𝐴 ·s 𝐵 ) } ∈ V
6 5 a1i ⊢ ( 𝜑 → { ( 𝐴 ·s 𝐵 ) } ∈ V )
7 eqid ⊢ ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) = ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
8 7 rnmpo ⊢ ran ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) = { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) }
9 sltsex1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ∈ V )
10 1 9 syl ⊢ ( 𝜑 → 𝐿 ∈ V )
11 sltsex2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ∈ V )
12 2 11 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
13 7 mpoexg ⊢ ( ( 𝐿 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V )
14 10 12 13 syl2anc ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V )
15 rnexg ⊢ ( ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V → ran ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V )
16 14 15 syl ⊢ ( 𝜑 → ran ( 𝑡 ∈ 𝐿 , 𝑢 ∈ 𝑆 ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V )
17 8 16 eqeltrrid ⊢ ( 𝜑 → { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∈ V )
18 eqid ⊢ ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) = ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
19 18 rnmpo ⊢ ran ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) = { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) }
20 sltsex2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ∈ V )
21 1 20 syl ⊢ ( 𝜑 → 𝑅 ∈ V )
22 sltsex1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ∈ V )
23 2 22 syl ⊢ ( 𝜑 → 𝑀 ∈ V )
24 18 mpoexg ⊢ ( ( 𝑅 ∈ V ∧ 𝑀 ∈ V ) → ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V )
25 21 23 24 syl2anc ⊢ ( 𝜑 → ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V )
26 rnexg ⊢ ( ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V → ran ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V )
27 25 26 syl ⊢ ( 𝜑 → ran ( 𝑣 ∈ 𝑅 , 𝑤 ∈ 𝑀 ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V )
28 19 27 eqeltrrid ⊢ ( 𝜑 → { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ∈ V )
29 17 28 unexd ⊢ ( 𝜑 → ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ∈ V )
30 1 cutscld ⊢ ( 𝜑 → ( 𝐿 |s 𝑅 ) ∈ No )
31 3 30 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ No )
32 2 cutscld ⊢ ( 𝜑 → ( 𝑀 |s 𝑆 ) ∈ No )
33 4 32 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ No )
34 31 33 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
35 34 snssd ⊢ ( 𝜑 → { ( 𝐴 ·s 𝐵 ) } ⊆ No )
36 sltsss1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ⊆ No )
37 1 36 syl ⊢ ( 𝜑 → 𝐿 ⊆ No )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐿 ⊆ No )
39 simprl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑡 ∈ 𝐿 )
40 38 39 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑡 ∈ No )
41 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐵 ∈ No )
42 40 41 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑡 ·s 𝐵 ) ∈ No )
43 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐴 ∈ No )
44 sltsss2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ⊆ No )
45 2 44 syl ⊢ ( 𝜑 → 𝑆 ⊆ No )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑆 ⊆ No )
47 simprr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑢 ∈ 𝑆 )
48 46 47 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑢 ∈ No )
49 43 48 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝐴 ·s 𝑢 ) ∈ No )
50 42 49 addscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) ∈ No )
51 40 48 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑡 ·s 𝑢 ) ∈ No )
52 50 51 subscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No )
53 eleq1 ⊢ ( 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( 𝑐 ∈ No ↔ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No ) )
54 52 53 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑐 ∈ No ) )
55 54 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑐 ∈ No ) )
56 55 abssdv ⊢ ( 𝜑 → { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ⊆ No )
57 sltsss2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ⊆ No )
58 1 57 syl ⊢ ( 𝜑 → 𝑅 ⊆ No )
59 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑅 ⊆ No )
60 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑣 ∈ 𝑅 )
61 59 60 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑣 ∈ No )
62 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝐵 ∈ No )
63 61 62 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝑣 ·s 𝐵 ) ∈ No )
64 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝐴 ∈ No )
65 sltsss1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ⊆ No )
66 2 65 syl ⊢ ( 𝜑 → 𝑀 ⊆ No )
67 66 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑀 ⊆ No )
68 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑤 ∈ 𝑀 )
69 67 68 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑤 ∈ No )
70 64 69 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝐴 ·s 𝑤 ) ∈ No )
71 63 70 addscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) ∈ No )
72 61 69 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝑣 ·s 𝑤 ) ∈ No )
73 71 72 subscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No )
74 eleq1 ⊢ ( 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( 𝑑 ∈ No ↔ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No ) )
75 73 74 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑑 ∈ No ) )
76 75 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑑 ∈ No ) )
77 76 abssdv ⊢ ( 𝜑 → { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ⊆ No )
78 56 77 unssd ⊢ ( 𝜑 → ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ⊆ No )
79 elun ⊢ ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ ( 𝑦 ∈ { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∨ 𝑦 ∈ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) )
80 vex ⊢ 𝑦 ∈ V
81 eqeq1 ⊢ ( 𝑐 = 𝑦 → ( 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
82 81 2rexbidv ⊢ ( 𝑐 = 𝑦 → ( ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
83 80 82 elab ⊢ ( 𝑦 ∈ { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ↔ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
84 eqeq1 ⊢ ( 𝑑 = 𝑦 → ( 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
85 84 2rexbidv ⊢ ( 𝑑 = 𝑦 → ( ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
86 80 85 elab ⊢ ( 𝑦 ∈ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ↔ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
87 83 86 orbi12i ⊢ ( ( 𝑦 ∈ { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∨ 𝑦 ∈ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ ( ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
88 79 87 bitri ⊢ ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ ( ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
89 cutcuts ⊢ ( 𝐿 <<s 𝑅 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
90 1 89 syl ⊢ ( 𝜑 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
91 90 simp2d ⊢ ( 𝜑 → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
92 91 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
93 ovex ⊢ ( 𝐿 |s 𝑅 ) ∈ V
94 93 snid ⊢ ( 𝐿 |s 𝑅 ) ∈ { ( 𝐿 |s 𝑅 ) }
95 3 94 eqeltrdi ⊢ ( 𝜑 → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
96 95 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
97 92 39 96 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑡 <s 𝐴 )
98 cutcuts ⊢ ( 𝑀 <<s 𝑆 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
99 2 98 syl ⊢ ( 𝜑 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
100 99 simp3d ⊢ ( 𝜑 → { ( 𝑀 |s 𝑆 ) } <<s 𝑆 )
101 100 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → { ( 𝑀 |s 𝑆 ) } <<s 𝑆 )
102 ovex ⊢ ( 𝑀 |s 𝑆 ) ∈ V
103 102 snid ⊢ ( 𝑀 |s 𝑆 ) ∈ { ( 𝑀 |s 𝑆 ) }
104 4 103 eqeltrdi ⊢ ( 𝜑 → 𝐵 ∈ { ( 𝑀 |s 𝑆 ) } )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐵 ∈ { ( 𝑀 |s 𝑆 ) } )
106 101 105 47 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → 𝐵 <s 𝑢 )
107 40 43 41 48 97 106 ltmulsd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑡 ·s 𝑢 ) -s ( 𝑡 ·s 𝐵 ) ) <s ( ( 𝐴 ·s 𝑢 ) -s ( 𝐴 ·s 𝐵 ) ) )
108 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
109 51 42 49 108 ltsubsubs2bd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ( 𝑡 ·s 𝑢 ) -s ( 𝑡 ·s 𝐵 ) ) <s ( ( 𝐴 ·s 𝑢 ) -s ( 𝐴 ·s 𝐵 ) ) ↔ ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑢 ) ) <s ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) ) )
110 42 51 subscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No )
111 108 49 110 ltsubaddsd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑢 ) ) <s ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) ↔ ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) +s ( 𝐴 ·s 𝑢 ) ) ) )
112 109 111 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ( 𝑡 ·s 𝑢 ) -s ( 𝑡 ·s 𝐵 ) ) <s ( ( 𝐴 ·s 𝑢 ) -s ( 𝐴 ·s 𝐵 ) ) ↔ ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) +s ( 𝐴 ·s 𝑢 ) ) ) )
113 107 112 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) +s ( 𝐴 ·s 𝑢 ) ) )
114 42 49 51 addsubsd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) = ( ( ( 𝑡 ·s 𝐵 ) -s ( 𝑡 ·s 𝑢 ) ) +s ( 𝐴 ·s 𝑢 ) ) )
115 113 114 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
116 breq2 ⊢ ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( 𝐴 ·s 𝐵 ) <s 𝑦 ↔ ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
117 115 116 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐿 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
118 117 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
119 90 simp3d ⊢ ( 𝜑 → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
120 119 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
121 95 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
122 120 121 60 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝐴 <s 𝑣 )
123 99 simp2d ⊢ ( 𝜑 → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
124 123 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
125 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝐵 ∈ { ( 𝑀 |s 𝑆 ) } )
126 124 68 125 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → 𝑤 <s 𝐵 )
127 64 61 69 62 122 126 ltmulsd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑤 ) ) <s ( ( 𝑣 ·s 𝐵 ) -s ( 𝑣 ·s 𝑤 ) ) )
128 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
129 63 72 subscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( ( 𝑣 ·s 𝐵 ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No )
130 128 70 129 ltsubaddsd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑤 ) ) <s ( ( 𝑣 ·s 𝐵 ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑣 ·s 𝐵 ) -s ( 𝑣 ·s 𝑤 ) ) +s ( 𝐴 ·s 𝑤 ) ) ) )
131 127 130 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑣 ·s 𝐵 ) -s ( 𝑣 ·s 𝑤 ) ) +s ( 𝐴 ·s 𝑤 ) ) )
132 63 70 72 addsubsd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) = ( ( ( 𝑣 ·s 𝐵 ) -s ( 𝑣 ·s 𝑤 ) ) +s ( 𝐴 ·s 𝑤 ) ) )
133 131 132 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
134 breq2 ⊢ ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( 𝐴 ·s 𝐵 ) <s 𝑦 ↔ ( 𝐴 ·s 𝐵 ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
135 133 134 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑤 ∈ 𝑀 ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
136 135 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
137 118 136 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
138 88 137 biimtrid ⊢ ( 𝜑 → ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
139 velsn ⊢ ( 𝑥 ∈ { ( 𝐴 ·s 𝐵 ) } ↔ 𝑥 = ( 𝐴 ·s 𝐵 ) )
140 breq1 ⊢ ( 𝑥 = ( 𝐴 ·s 𝐵 ) → ( 𝑥 <s 𝑦 ↔ ( 𝐴 ·s 𝐵 ) <s 𝑦 ) )
141 140 imbi2d ⊢ ( 𝑥 = ( 𝐴 ·s 𝐵 ) → ( ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) → 𝑥 <s 𝑦 ) ↔ ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) ) )
142 139 141 sylbi ⊢ ( 𝑥 ∈ { ( 𝐴 ·s 𝐵 ) } → ( ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) → 𝑥 <s 𝑦 ) ↔ ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) → ( 𝐴 ·s 𝐵 ) <s 𝑦 ) ) )
143 138 142 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 ∈ { ( 𝐴 ·s 𝐵 ) } → ( 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) → 𝑥 <s 𝑦 ) ) )
144 143 3imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ( 𝐴 ·s 𝐵 ) } ∧ 𝑦 ∈ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) → 𝑥 <s 𝑦 )
145 6 29 35 78 144 sltsd ⊢ ( 𝜑 → { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) )