Metamath Proof Explorer

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 
|- ( ph -> L <
mulsunif2.2 
|- ( ph -> M <
mulsunif2.3 
|- ( ph -> A = ( L |s R ) )
mulsunif2.4 
|- ( ph -> B = ( M |s S ) )
Assertion mulsunif2lem 
|- ( 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 ) ) ) } ) ) )

Proof

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