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	$⊢ φ \to L ≪_{s} R$
	sltmuls2.2	$⊢ φ \to M ≪_{s} S$
	sltmuls2.3	$⊢ φ \to A = L \|_{s} R$
	sltmuls2.4	$⊢ φ \to B = M \|_{s} S$
Assertion	sltmuls2	$⊢ φ \to \{A \cdot_{s} B\} ≪_{s} (\{c \| \exists t \in L \exists u \in S c = ((t \cdot_{s} B) +_{s} (A \cdot_{s} u)) -_{s} (t \cdot_{s} u)\} \cup \{d \| \exists v \in R \exists w \in M d = ((v \cdot_{s} B) +_{s} (A \cdot_{s} w)) -_{s} (v \cdot_{s} w)\})$

Proof

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

Metamath Proof Explorer

Theorem sltmuls2

Proof