mulsunif2lem

Description: Lemma for mulsunif2 . State the theorem with extra disjoint variable conditions. (Contributed by Scott Fenton, 16-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		mulsunif2.1	$⊢ φ \to L ≪_{s} R$
2		mulsunif2.2	$⊢ φ \to M ≪_{s} S$
3		mulsunif2.3	$⊢ φ \to A = L \|_{s} R$
4		mulsunif2.4	$⊢ φ \to B = M \|_{s} S$
5	1 2 3 4	mulsunif	$⊢ φ \to A \cdot_{s} B = (\{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} (\{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)\})$
6	1	cutscld	$⊢ φ \to L \|_{s} R \in No$
7	3 6	eqeltrd	$⊢ φ \to A \in No$
8	2	cutscld	$⊢ φ \to M \|_{s} S \in No$
9	4 8	eqeltrd	$⊢ φ \to B \in No$
10	7 9	mulscld	$⊢ φ \to A \cdot_{s} B \in No$
11	10	adantr	$⊢ (φ \land (p \in L \land q \in M)) \to A \cdot_{s} B \in No$
12		sltsss1	$⊢ L ≪_{s} R \to L \subseteq No$
13	1 12	syl	$⊢ φ \to L \subseteq No$
14	13	sselda	$⊢ (φ \land p \in L) \to p \in No$
15	14	adantrr	$⊢ (φ \land (p \in L \land q \in M)) \to p \in No$
16	9	adantr	$⊢ (φ \land (p \in L \land q \in M)) \to B \in No$
17	15 16	mulscld	$⊢ (φ \land (p \in L \land q \in M)) \to p \cdot_{s} B \in No$
18	7	adantr	$⊢ (φ \land (p \in L \land q \in M)) \to A \in No$
19		sltsss1	$⊢ M ≪_{s} S \to M \subseteq No$
20	2 19	syl	$⊢ φ \to M \subseteq No$
21	20	sselda	$⊢ (φ \land q \in M) \to q \in No$
22	21	adantrl	$⊢ (φ \land (p \in L \land q \in M)) \to q \in No$
23	18 22	mulscld	$⊢ (φ \land (p \in L \land q \in M)) \to A \cdot_{s} q \in No$
24	15 22	mulscld	$⊢ (φ \land (p \in L \land q \in M)) \to p \cdot_{s} q \in No$
25	23 24	subscld	$⊢ (φ \land (p \in L \land q \in M)) \to (A \cdot_{s} q) -_{s} (p \cdot_{s} q) \in No$
26	11 17 25	subsubs4d	$⊢ (φ \land (p \in L \land q \in M)) \to ((A \cdot_{s} B) -_{s} (p \cdot_{s} B)) -_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q)) = (A \cdot_{s} B) -_{s} ((p \cdot_{s} B) +_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q)))$
27	26	oveq2d	$⊢ (φ \land (p \in L \land q \in M)) \to (A \cdot_{s} B) -_{s} (((A \cdot_{s} B) -_{s} (p \cdot_{s} B)) -_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))) = (A \cdot_{s} B) -_{s} ((A \cdot_{s} B) -_{s} ((p \cdot_{s} B) +_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))))$
28	17 25	addscld	$⊢ (φ \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$
29	11 28	nncansd	$⊢ (φ \land (p \in L \land q \in M)) \to (A \cdot_{s} B) -_{s} ((A \cdot_{s} B) -_{s} ((p \cdot_{s} B) +_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q)))) = (p \cdot_{s} B) +_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))$
30	27 29	eqtrd	$⊢ (φ \land (p \in L \land q \in M)) \to (A \cdot_{s} B) -_{s} (((A \cdot_{s} B) -_{s} (p \cdot_{s} B)) -_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))) = (p \cdot_{s} B) +_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))$
31	18 15	subscld	$⊢ (φ \land (p \in L \land q \in M)) \to A -_{s} p \in No$
32	31 16 22	subsdid	$⊢ (φ \land (p \in L \land q \in M)) \to (A -_{s} p) \cdot_{s} (B -_{s} q) = ((A -_{s} p) \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} q)$
33	18 15 16	subsdird	$⊢ (φ \land (p \in L \land q \in M)) \to (A -_{s} p) \cdot_{s} B = (A \cdot_{s} B) -_{s} (p \cdot_{s} B)$
34	18 15 22	subsdird	$⊢ (φ \land (p \in L \land q \in M)) \to (A -_{s} p) \cdot_{s} q = (A \cdot_{s} q) -_{s} (p \cdot_{s} q)$
35	33 34	oveq12d	$⊢ (φ \land (p \in L \land q \in M)) \to ((A -_{s} p) \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} q) = ((A \cdot_{s} B) -_{s} (p \cdot_{s} B)) -_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))$
36	32 35	eqtrd	$⊢ (φ \land (p \in L \land q \in M)) \to (A -_{s} p) \cdot_{s} (B -_{s} q) = ((A \cdot_{s} B) -_{s} (p \cdot_{s} B)) -_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))$
37	36	oveq2d	$⊢ (φ \land (p \in L \land q \in M)) \to (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q)) = (A \cdot_{s} B) -_{s} (((A \cdot_{s} B) -_{s} (p \cdot_{s} B)) -_{s} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q)))$
38	17 23 24	addsubsassd	$⊢ (φ \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} ((A \cdot_{s} q) -_{s} (p \cdot_{s} q))$
39	30 37 38	3eqtr4rd	$⊢ (φ \land (p \in L \land q \in M)) \to ((p \cdot_{s} B) +_{s} (A \cdot_{s} q)) -_{s} (p \cdot_{s} q) = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))$
40	39	eqeq2d	$⊢ (φ \land (p \in L \land q \in M)) \to (a = ((p \cdot_{s} B) +_{s} (A \cdot_{s} q)) -_{s} (p \cdot_{s} q) \leftrightarrow a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q)))$
41	40	2rexbidva	$⊢ φ \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 a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q)))$
42	41	abbidv	$⊢ φ \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)\} = \{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\}$
43	10	adantr	$⊢ (φ \land (r \in R \land s \in S)) \to A \cdot_{s} B \in No$
44		sltsss2	$⊢ L ≪_{s} R \to R \subseteq No$
45	1 44	syl	$⊢ φ \to R \subseteq No$
46	45	sselda	$⊢ (φ \land r \in R) \to r \in No$
47	46	adantrr	$⊢ (φ \land (r \in R \land s \in S)) \to r \in No$
48		sltsss2	$⊢ M ≪_{s} S \to S \subseteq No$
49	2 48	syl	$⊢ φ \to S \subseteq No$
50	49	sselda	$⊢ (φ \land s \in S) \to s \in No$
51	50	adantrl	$⊢ (φ \land (r \in R \land s \in S)) \to s \in No$
52	47 51	mulscld	$⊢ (φ \land (r \in R \land s \in S)) \to r \cdot_{s} s \in No$
53	7	adantr	$⊢ (φ \land (r \in R \land s \in S)) \to A \in No$
54	53 51	mulscld	$⊢ (φ \land (r \in R \land s \in S)) \to A \cdot_{s} s \in No$
55	52 54	subscld	$⊢ (φ \land (r \in R \land s \in S)) \to (r \cdot_{s} s) -_{s} (A \cdot_{s} s) \in No$
56	9	adantr	$⊢ (φ \land (r \in R \land s \in S)) \to B \in No$
57	47 56	mulscld	$⊢ (φ \land (r \in R \land s \in S)) \to r \cdot_{s} B \in No$
58	57 43	subscld	$⊢ (φ \land (r \in R \land s \in S)) \to (r \cdot_{s} B) -_{s} (A \cdot_{s} B) \in No$
59	43 55 58	subsubs2d	$⊢ (φ \land (r \in R \land s \in S)) \to (A \cdot_{s} B) -_{s} (((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) -_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B))) = (A \cdot_{s} B) +_{s} (((r \cdot_{s} B) -_{s} (A \cdot_{s} B)) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)))$
60	43 58 55	addsubsassd	$⊢ (φ \land (r \in R \land s \in S)) \to ((A \cdot_{s} B) +_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B))) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) = (A \cdot_{s} B) +_{s} (((r \cdot_{s} B) -_{s} (A \cdot_{s} B)) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)))$
61		pncan3s	$⊢ (A \cdot_{s} B \in No \land r \cdot_{s} B \in No) \to (A \cdot_{s} B) +_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B)) = r \cdot_{s} B$
62	43 57 61	syl2anc	$⊢ (φ \land (r \in R \land s \in S)) \to (A \cdot_{s} B) +_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B)) = r \cdot_{s} B$
63	62	oveq1d	$⊢ (φ \land (r \in R \land s \in S)) \to ((A \cdot_{s} B) +_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B))) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) = (r \cdot_{s} B) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s))$
64	59 60 63	3eqtr2d	$⊢ (φ \land (r \in R \land s \in S)) \to (A \cdot_{s} B) -_{s} (((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) -_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B))) = (r \cdot_{s} B) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s))$
65	47 53	subscld	$⊢ (φ \land (r \in R \land s \in S)) \to r -_{s} A \in No$
66	65 51 56	subsdid	$⊢ (φ \land (r \in R \land s \in S)) \to (r -_{s} A) \cdot_{s} (s -_{s} B) = ((r -_{s} A) \cdot_{s} s) -_{s} ((r -_{s} A) \cdot_{s} B)$
67	47 53 51	subsdird	$⊢ (φ \land (r \in R \land s \in S)) \to (r -_{s} A) \cdot_{s} s = (r \cdot_{s} s) -_{s} (A \cdot_{s} s)$
68	47 53 56	subsdird	$⊢ (φ \land (r \in R \land s \in S)) \to (r -_{s} A) \cdot_{s} B = (r \cdot_{s} B) -_{s} (A \cdot_{s} B)$
69	67 68	oveq12d	$⊢ (φ \land (r \in R \land s \in S)) \to ((r -_{s} A) \cdot_{s} s) -_{s} ((r -_{s} A) \cdot_{s} B) = ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) -_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B))$
70	66 69	eqtrd	$⊢ (φ \land (r \in R \land s \in S)) \to (r -_{s} A) \cdot_{s} (s -_{s} B) = ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) -_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B))$
71	70	oveq2d	$⊢ (φ \land (r \in R \land s \in S)) \to (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B)) = (A \cdot_{s} B) -_{s} (((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) -_{s} ((r \cdot_{s} B) -_{s} (A \cdot_{s} B)))$
72	57 54 52	addsubsassd	$⊢ (φ \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} ((A \cdot_{s} s) -_{s} (r \cdot_{s} s))$
73	57 52 54	subsubs2d	$⊢ (φ \land (r \in R \land s \in S)) \to (r \cdot_{s} B) -_{s} ((r \cdot_{s} s) -_{s} (A \cdot_{s} s)) = (r \cdot_{s} B) +_{s} ((A \cdot_{s} s) -_{s} (r \cdot_{s} s))$
74	72 73	eqtr4d	$⊢ (φ \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))$
75	64 71 74	3eqtr4rd	$⊢ (φ \land (r \in R \land s \in S)) \to ((r \cdot_{s} B) +_{s} (A \cdot_{s} s)) -_{s} (r \cdot_{s} s) = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))$
76	75	eqeq2d	$⊢ (φ \land (r \in R \land s \in S)) \to (b = ((r \cdot_{s} B) +_{s} (A \cdot_{s} s)) -_{s} (r \cdot_{s} s) \leftrightarrow b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B)))$
77	76	2rexbidva	$⊢ φ \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 b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B)))$
78	77	abbidv	$⊢ φ \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)\} = \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}$
79	42 78	uneq12d	$⊢ φ \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)\} = \{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}$
80	7	adantr	$⊢ (φ \land (t \in L \land u \in S)) \to A \in No$
81	49	sselda	$⊢ (φ \land u \in S) \to u \in No$
82	81	adantrl	$⊢ (φ \land (t \in L \land u \in S)) \to u \in No$
83	80 82	mulscld	$⊢ (φ \land (t \in L \land u \in S)) \to A \cdot_{s} u \in No$
84	10	adantr	$⊢ (φ \land (t \in L \land u \in S)) \to A \cdot_{s} B \in No$
85	83 84	subscld	$⊢ (φ \land (t \in L \land u \in S)) \to (A \cdot_{s} u) -_{s} (A \cdot_{s} B) \in No$
86	13	sselda	$⊢ (φ \land t \in L) \to t \in No$
87	86	adantrr	$⊢ (φ \land (t \in L \land u \in S)) \to t \in No$
88	87 82	mulscld	$⊢ (φ \land (t \in L \land u \in S)) \to t \cdot_{s} u \in No$
89	9	adantr	$⊢ (φ \land (t \in L \land u \in S)) \to B \in No$
90	87 89	mulscld	$⊢ (φ \land (t \in L \land u \in S)) \to t \cdot_{s} B \in No$
91	85 88 90	subsubs2d	$⊢ (φ \land (t \in L \land u \in S)) \to ((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B)) = ((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
92	90 88	subscld	$⊢ (φ \land (t \in L \land u \in S)) \to (t \cdot_{s} B) -_{s} (t \cdot_{s} u) \in No$
93	83 92 84	addsubsd	$⊢ (φ \land (t \in L \land u \in S)) \to ((A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))) -_{s} (A \cdot_{s} B) = ((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
94	91 93	eqtr4d	$⊢ (φ \land (t \in L \land u \in S)) \to ((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B)) = ((A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))) -_{s} (A \cdot_{s} B)$
95	94	oveq2d	$⊢ (φ \land (t \in L \land u \in S)) \to (A \cdot_{s} B) +_{s} (((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B))) = (A \cdot_{s} B) +_{s} (((A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))) -_{s} (A \cdot_{s} B))$
96	83 92	addscld	$⊢ (φ \land (t \in L \land u \in S)) \to (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u)) \in No$
97		pncan3s	$⊢ (A \cdot_{s} B \in No \land (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u)) \in No) \to (A \cdot_{s} B) +_{s} (((A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))) -_{s} (A \cdot_{s} B)) = (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
98	84 96 97	syl2anc	$⊢ (φ \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))) -_{s} (A \cdot_{s} B)) = (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
99	95 98	eqtrd	$⊢ (φ \land (t \in L \land u \in S)) \to (A \cdot_{s} B) +_{s} (((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B))) = (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
100	82 89	subscld	$⊢ (φ \land (t \in L \land u \in S)) \to u -_{s} B \in No$
101	80 87 100	subsdird	$⊢ (φ \land (t \in L \land u \in S)) \to (A -_{s} t) \cdot_{s} (u -_{s} B) = (A \cdot_{s} (u -_{s} B)) -_{s} (t \cdot_{s} (u -_{s} B))$
102	80 82 89	subsdid	$⊢ (φ \land (t \in L \land u \in S)) \to A \cdot_{s} (u -_{s} B) = (A \cdot_{s} u) -_{s} (A \cdot_{s} B)$
103	87 82 89	subsdid	$⊢ (φ \land (t \in L \land u \in S)) \to t \cdot_{s} (u -_{s} B) = (t \cdot_{s} u) -_{s} (t \cdot_{s} B)$
104	102 103	oveq12d	$⊢ (φ \land (t \in L \land u \in S)) \to (A \cdot_{s} (u -_{s} B)) -_{s} (t \cdot_{s} (u -_{s} B)) = ((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B))$
105	101 104	eqtrd	$⊢ (φ \land (t \in L \land u \in S)) \to (A -_{s} t) \cdot_{s} (u -_{s} B) = ((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B))$
106	105	oveq2d	$⊢ (φ \land (t \in L \land u \in S)) \to (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B)) = (A \cdot_{s} B) +_{s} (((A \cdot_{s} u) -_{s} (A \cdot_{s} B)) -_{s} ((t \cdot_{s} u) -_{s} (t \cdot_{s} B)))$
107	90 83	addscomd	$⊢ (φ \land (t \in L \land u \in S)) \to (t \cdot_{s} B) +_{s} (A \cdot_{s} u) = (A \cdot_{s} u) +_{s} (t \cdot_{s} B)$
108	107	oveq1d	$⊢ (φ \land (t \in L \land u \in S)) \to ((t \cdot_{s} B) +_{s} (A \cdot_{s} u)) -_{s} (t \cdot_{s} u) = ((A \cdot_{s} u) +_{s} (t \cdot_{s} B)) -_{s} (t \cdot_{s} u)$
109	83 90 88	addsubsassd	$⊢ (φ \land (t \in L \land u \in S)) \to ((A \cdot_{s} u) +_{s} (t \cdot_{s} B)) -_{s} (t \cdot_{s} u) = (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
110	108 109	eqtrd	$⊢ (φ \land (t \in L \land u \in S)) \to ((t \cdot_{s} B) +_{s} (A \cdot_{s} u)) -_{s} (t \cdot_{s} u) = (A \cdot_{s} u) +_{s} ((t \cdot_{s} B) -_{s} (t \cdot_{s} u))$
111	99 106 110	3eqtr4rd	$⊢ (φ \land (t \in L \land u \in S)) \to ((t \cdot_{s} B) +_{s} (A \cdot_{s} u)) -_{s} (t \cdot_{s} u) = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))$
112	111	eqeq2d	$⊢ (φ \land (t \in L \land u \in S)) \to (c = ((t \cdot_{s} B) +_{s} (A \cdot_{s} u)) -_{s} (t \cdot_{s} u) \leftrightarrow c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B)))$
113	112	2rexbidva	$⊢ φ \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 c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B)))$
114	113	abbidv	$⊢ φ \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)\} = \{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\}$
115	45	sselda	$⊢ (φ \land v \in R) \to v \in No$
116	115	adantrr	$⊢ (φ \land (v \in R \land w \in M)) \to v \in No$
117	9	adantr	$⊢ (φ \land (v \in R \land w \in M)) \to B \in No$
118	116 117	mulscld	$⊢ (φ \land (v \in R \land w \in M)) \to v \cdot_{s} B \in No$
119	20	sselda	$⊢ (φ \land w \in M) \to w \in No$
120	119	adantrl	$⊢ (φ \land (v \in R \land w \in M)) \to w \in No$
121	116 120	mulscld	$⊢ (φ \land (v \in R \land w \in M)) \to v \cdot_{s} w \in No$
122	118 121	subscld	$⊢ (φ \land (v \in R \land w \in M)) \to (v \cdot_{s} B) -_{s} (v \cdot_{s} w) \in No$
123	10	adantr	$⊢ (φ \land (v \in R \land w \in M)) \to A \cdot_{s} B \in No$
124	7	adantr	$⊢ (φ \land (v \in R \land w \in M)) \to A \in No$
125	124 120	mulscld	$⊢ (φ \land (v \in R \land w \in M)) \to A \cdot_{s} w \in No$
126	122 123 125	subsubs2d	$⊢ (φ \land (v \in R \land w \in M)) \to ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) -_{s} ((A \cdot_{s} B) -_{s} (A \cdot_{s} w)) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} ((A \cdot_{s} w) -_{s} (A \cdot_{s} B))$
127	122 125 123	addsubsassd	$⊢ (φ \land (v \in R \land w \in M)) \to (((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)) -_{s} (A \cdot_{s} B) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} ((A \cdot_{s} w) -_{s} (A \cdot_{s} B))$
128	126 127	eqtr4d	$⊢ (φ \land (v \in R \land w \in M)) \to ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) -_{s} ((A \cdot_{s} B) -_{s} (A \cdot_{s} w)) = (((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)) -_{s} (A \cdot_{s} B)$
129	128	oveq2d	$⊢ (φ \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} B) -_{s} (A \cdot_{s} w))) = (A \cdot_{s} B) +_{s} ((((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)) -_{s} (A \cdot_{s} B))$
130	122 125	addscld	$⊢ (φ \land (v \in R \land w \in M)) \to ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w) \in No$
131		pncan3s	$⊢ (A \cdot_{s} B \in No \land ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w) \in No) \to (A \cdot_{s} B) +_{s} ((((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)) -_{s} (A \cdot_{s} B)) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)$
132	123 130 131	syl2anc	$⊢ (φ \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)) -_{s} (A \cdot_{s} B)) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)$
133	129 132	eqtrd	$⊢ (φ \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} B) -_{s} (A \cdot_{s} w))) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) +_{s} (A \cdot_{s} w)$
134	117 120	subscld	$⊢ (φ \land (v \in R \land w \in M)) \to B -_{s} w \in No$
135	116 124 134	subsdird	$⊢ (φ \land (v \in R \land w \in M)) \to (v -_{s} A) \cdot_{s} (B -_{s} w) = (v \cdot_{s} (B -_{s} w)) -_{s} (A \cdot_{s} (B -_{s} w))$
136	116 117 120	subsdid	$⊢ (φ \land (v \in R \land w \in M)) \to v \cdot_{s} (B -_{s} w) = (v \cdot_{s} B) -_{s} (v \cdot_{s} w)$
137	124 117 120	subsdid	$⊢ (φ \land (v \in R \land w \in M)) \to A \cdot_{s} (B -_{s} w) = (A \cdot_{s} B) -_{s} (A \cdot_{s} w)$
138	136 137	oveq12d	$⊢ (φ \land (v \in R \land w \in M)) \to (v \cdot_{s} (B -_{s} w)) -_{s} (A \cdot_{s} (B -_{s} w)) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) -_{s} ((A \cdot_{s} B) -_{s} (A \cdot_{s} w))$
139	135 138	eqtrd	$⊢ (φ \land (v \in R \land w \in M)) \to (v -_{s} A) \cdot_{s} (B -_{s} w) = ((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) -_{s} ((A \cdot_{s} B) -_{s} (A \cdot_{s} w))$
140	139	oveq2d	$⊢ (φ \land (v \in R \land w \in M)) \to (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w)) = (A \cdot_{s} B) +_{s} (((v \cdot_{s} B) -_{s} (v \cdot_{s} w)) -_{s} ((A \cdot_{s} B) -_{s} (A \cdot_{s} w)))$
141	118 125 121	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)$
142	133 140 141	3eqtr4rd	$⊢ (φ \land (v \in R \land w \in M)) \to ((v \cdot_{s} B) +_{s} (A \cdot_{s} w)) -_{s} (v \cdot_{s} w) = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))$
143	142	eqeq2d	$⊢ (φ \land (v \in R \land w \in M)) \to (d = ((v \cdot_{s} B) +_{s} (A \cdot_{s} w)) -_{s} (v \cdot_{s} w) \leftrightarrow d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w)))$
144	143	2rexbidva	$⊢ φ \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 d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w)))$
145	144	abbidv	$⊢ φ \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)\} = \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\}$
146	114 145	uneq12d	$⊢ φ \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)\} = \{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\}$
147	79 146	oveq12d	$⊢ φ \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} (\{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)\}) = (\{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}) \|_{s} (\{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\})$
148	5 147	eqtrd	$⊢ φ \to A \cdot_{s} B = (\{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}) \|_{s} (\{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\})$

Metamath Proof Explorer

Theorem mulsunif2lem

Proof