ssltmul1

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

	Ref	Expression
Hypotheses	ssltmul1.1	$⊢ φ \to L ≪_{s} R$
	ssltmul1.2	$⊢ φ \to M ≪_{s} S$
	ssltmul1.3	$⊢ φ \to A = L \|_{s} R$
	ssltmul1.4	$⊢ φ \to B = M \|_{s} S$
Assertion	ssltmul1	$⊢ φ \to (\{a \| \exists p \in L \exists q \in M a = ((p \cdot_{s} B) +_{s} (A \cdot_{s} q)) -_{s} (p \cdot_{s} q)\} \cup \{b \| \exists r \in R \exists s \in S b = ((r \cdot_{s} B) +_{s} (A \cdot_{s} s)) -_{s} (r \cdot_{s} s)\}) ≪_{s} \{A \cdot_{s} B\}$

Proof

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

Metamath Proof Explorer

Theorem ssltmul1

Proof