Metamath Proof Explorer


Theorem mulsrid

Description: Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion mulsrid A No A s 1 s = A

Proof

Step Hyp Ref Expression
1 oveq1 Could not format ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) ) : No typesetting found for |- ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) ) with typecode |-
2 id Could not format ( x = xO -> x = xO ) : No typesetting found for |- ( x = xO -> x = xO ) with typecode |-
3 1 2 eqeq12d Could not format ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) ) with typecode |-
4 oveq1 x = A x s 1 s = A s 1 s
5 id x = A x = A
6 4 5 eqeq12d x = A x s 1 s = x A s 1 s = A
7 1sno 1 s No
8 mulsval x No 1 s No x s 1 s = a | p L x q L 1 s a = p s 1 s + s x s q - s p s q b | r R x s R 1 s b = r s 1 s + s x s s - s r s s | s c | t L x u R 1 s c = t s 1 s + s x s u - s t s u d | v R x w L 1 s d = v s 1 s + s x s w - s v s w
9 7 8 mpan2 x No x s 1 s = a | p L x q L 1 s a = p s 1 s + s x s q - s p s q b | r R x s R 1 s b = r s 1 s + s x s s - s r s s | s c | t L x u R 1 s c = t s 1 s + s x s u - s t s u d | v R x w L 1 s d = v s 1 s + s x s w - s v s w
10 9 adantr Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
11 elun1 p L x p L x R x
12 oveq1 Could not format ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) ) : No typesetting found for |- ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) ) with typecode |-
13 id Could not format ( xO = p -> xO = p ) : No typesetting found for |- ( xO = p -> xO = p ) with typecode |-
14 12 13 eqeq12d Could not format ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) ) with typecode |-
15 14 rspcva Could not format ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) with typecode |-
16 11 15 sylan Could not format ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) with typecode |-
17 16 ancoms Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) with typecode |-
18 17 adantll Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) with typecode |-
19 muls01 x No x s 0 s = 0 s
20 19 adantr Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s ) with typecode |-
21 20 adantr Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s ) with typecode |-
22 18 21 oveq12d Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) ) with typecode |-
23 leftssno L x No
24 23 sseli p L x p No
25 24 adantl Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No ) with typecode |-
26 25 addsridd Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p ) with typecode |-
27 22 26 eqtrd Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p ) with typecode |-
28 muls01 p No p s 0 s = 0 s
29 25 28 syl Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s ) with typecode |-
30 27 29 oveq12d Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) ) with typecode |-
31 subsid1 p No p - s 0 s = p
32 25 31 syl Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p ) with typecode |-
33 30 32 eqtrd Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p ) with typecode |-
34 33 eqeq2d Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) ) with typecode |-
35 equcom a = p p = a
36 34 35 bitrdi Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) ) with typecode |-
37 36 rexbidva Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) ) with typecode |-
38 left1s L 1 s = 0 s
39 38 rexeqi q L 1 s a = p s 1 s + s x s q - s p s q q 0 s a = p s 1 s + s x s q - s p s q
40 0sno 0 s No
41 40 elexi 0 s V
42 oveq2 q = 0 s x s q = x s 0 s
43 42 oveq2d q = 0 s p s 1 s + s x s q = p s 1 s + s x s 0 s
44 oveq2 q = 0 s p s q = p s 0 s
45 43 44 oveq12d q = 0 s p s 1 s + s x s q - s p s q = p s 1 s + s x s 0 s - s p s 0 s
46 45 eqeq2d q = 0 s a = p s 1 s + s x s q - s p s q a = p s 1 s + s x s 0 s - s p s 0 s
47 41 46 rexsn q 0 s a = p s 1 s + s x s q - s p s q a = p s 1 s + s x s 0 s - s p s 0 s
48 39 47 bitri q L 1 s a = p s 1 s + s x s q - s p s q a = p s 1 s + s x s 0 s - s p s 0 s
49 48 rexbii p L x q L 1 s a = p s 1 s + s x s q - s p s q p L x a = p s 1 s + s x s 0 s - s p s 0 s
50 risset a L x p L x p = a
51 37 49 50 3bitr4g Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) ) with typecode |-
52 51 eqabcdv Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) ) with typecode |-
53 rex0 ¬ s b = r s 1 s + s x s s - s r s s
54 right1s R 1 s =
55 54 rexeqi s R 1 s b = r s 1 s + s x s s - s r s s s b = r s 1 s + s x s s - s r s s
56 53 55 mtbir ¬ s R 1 s b = r s 1 s + s x s s - s r s s
57 56 a1i r R x ¬ s R 1 s b = r s 1 s + s x s s - s r s s
58 57 nrex ¬ r R x s R 1 s b = r s 1 s + s x s s - s r s s
59 58 abf b | r R x s R 1 s b = r s 1 s + s x s s - s r s s =
60 59 a1i Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) ) with typecode |-
61 52 60 uneq12d Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) ) with typecode |-
62 un0 L x = L x
63 61 62 eqtrdi Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) ) with typecode |-
64 rex0 ¬ u c = t s 1 s + s x s u - s t s u
65 54 rexeqi u R 1 s c = t s 1 s + s x s u - s t s u u c = t s 1 s + s x s u - s t s u
66 64 65 mtbir ¬ u R 1 s c = t s 1 s + s x s u - s t s u
67 66 a1i t L x ¬ u R 1 s c = t s 1 s + s x s u - s t s u
68 67 nrex ¬ t L x u R 1 s c = t s 1 s + s x s u - s t s u
69 68 abf c | t L x u R 1 s c = t s 1 s + s x s u - s t s u =
70 69 a1i Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) ) with typecode |-
71 elun2 v R x v L x R x
72 oveq1 Could not format ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) ) : No typesetting found for |- ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) ) with typecode |-
73 id Could not format ( xO = v -> xO = v ) : No typesetting found for |- ( xO = v -> xO = v ) with typecode |-
74 72 73 eqeq12d Could not format ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) ) with typecode |-
75 74 rspcva Could not format ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) with typecode |-
76 71 75 sylan Could not format ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) with typecode |-
77 76 ancoms Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) with typecode |-
78 77 adantll Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) with typecode |-
79 20 adantr Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s ) with typecode |-
80 78 79 oveq12d Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) ) with typecode |-
81 rightssno R x No
82 81 sseli v R x v No
83 82 adantl Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No ) with typecode |-
84 83 addsridd Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v ) with typecode |-
85 80 84 eqtrd Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v ) with typecode |-
86 muls01 v No v s 0 s = 0 s
87 83 86 syl Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s ) with typecode |-
88 85 87 oveq12d Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) ) with typecode |-
89 subsid1 v No v - s 0 s = v
90 83 89 syl Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v ) with typecode |-
91 88 90 eqtrd Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v ) with typecode |-
92 91 eqeq2d Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) ) with typecode |-
93 38 rexeqi w L 1 s d = v s 1 s + s x s w - s v s w w 0 s d = v s 1 s + s x s w - s v s w
94 oveq2 w = 0 s x s w = x s 0 s
95 94 oveq2d w = 0 s v s 1 s + s x s w = v s 1 s + s x s 0 s
96 oveq2 w = 0 s v s w = v s 0 s
97 95 96 oveq12d w = 0 s v s 1 s + s x s w - s v s w = v s 1 s + s x s 0 s - s v s 0 s
98 97 eqeq2d w = 0 s d = v s 1 s + s x s w - s v s w d = v s 1 s + s x s 0 s - s v s 0 s
99 41 98 rexsn w 0 s d = v s 1 s + s x s w - s v s w d = v s 1 s + s x s 0 s - s v s 0 s
100 93 99 bitri w L 1 s d = v s 1 s + s x s w - s v s w d = v s 1 s + s x s 0 s - s v s 0 s
101 equcom v = d d = v
102 92 100 101 3bitr4g Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) ) with typecode |-
103 102 rexbidva Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) ) with typecode |-
104 risset d R x v R x v = d
105 103 104 bitr4di Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) ) with typecode |-
106 105 eqabcdv Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) ) with typecode |-
107 70 106 uneq12d Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) ) with typecode |-
108 0un R x = R x
109 107 108 eqtrdi Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) ) with typecode |-
110 63 109 oveq12d Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) with typecode |-
111 lrcut x No L x | s R x = x
112 111 adantr Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) with typecode |-
113 10 110 112 3eqtrd Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x ) with typecode |-
114 113 ex Could not format ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) ) : No typesetting found for |- ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) ) with typecode |-
115 3 6 114 noinds A No A s 1 s = A