Theorem 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	$$⊢\phi \to L{\ll }_{s}R$$
	mulsunif2.2	$$⊢\phi \to M{\ll }_{s}S$$
	mulsunif2.3	$$⊢\phi \to A=L{|}_{s}R$$
	mulsunif2.4	$$⊢\phi \to B=M{|}_{s}S$$
Assertion	mulsunif2lem	Could not format assertion : No typesetting found for |- ( ph -> ( A x.s B ) = ( ( { a | E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) } u. { b | E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { d | E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) } ) ) ) with typecode |-

Proof

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