Step |
Hyp |
Ref |
Expression |
1 |
|
dfgrp3.b |
|
2 |
|
dfgrp3.p |
|
3 |
|
simp2 |
Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> B =/= (/) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> B =/= (/) ) with typecode |- |
4 |
|
n0 |
|
5 |
3 4
|
sylib |
Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. w w e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. w w e. B ) with typecode |- |
6 |
|
oveq2 |
|
7 |
6
|
eqeq1d |
|
8 |
7
|
rexbidv |
|
9 |
|
oveq1 |
|
10 |
9
|
eqeq1d |
|
11 |
10
|
rexbidv |
|
12 |
8 11
|
anbi12d |
|
13 |
12
|
ralbidv |
|
14 |
13
|
rspcv |
|
15 |
|
eqeq2 |
|
16 |
15
|
rexbidv |
|
17 |
|
eqeq2 |
|
18 |
17
|
rexbidv |
|
19 |
16 18
|
anbi12d |
|
20 |
19
|
rspcva |
|
21 |
|
oveq1 |
|
22 |
21
|
eqeq1d |
|
23 |
22
|
cbvrexvw |
|
24 |
23
|
biimpi |
|
25 |
24
|
adantr |
|
26 |
20 25
|
syl |
|
27 |
26
|
ex |
|
28 |
14 27
|
syldc |
|
29 |
28
|
3ad2ant3 |
Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( w e. B -> E. u e. B ( u .+ w ) = w ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( w e. B -> E. u e. B ( u .+ w ) = w ) ) with typecode |- |
30 |
29
|
imp |
Could not format ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) -> E. u e. B ( u .+ w ) = w ) : No typesetting found for |- ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) -> E. u e. B ( u .+ w ) = w ) with typecode |- |
31 |
|
eqeq2 |
|
32 |
31
|
rexbidv |
|
33 |
|
eqeq2 |
|
34 |
33
|
rexbidv |
|
35 |
32 34
|
anbi12d |
|
36 |
12 35
|
rspc2va |
|
37 |
36
|
simprd |
|
38 |
37
|
expcom |
|
39 |
38
|
3ad2ant3 |
Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( w e. B /\ a e. B ) -> E. r e. B ( w .+ r ) = a ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( w e. B /\ a e. B ) -> E. r e. B ( w .+ r ) = a ) ) with typecode |- |
40 |
39
|
impl |
Could not format ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ a e. B ) -> E. r e. B ( w .+ r ) = a ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ a e. B ) -> E. r e. B ( w .+ r ) = a ) with typecode |- |
41 |
40
|
ad2ant2r |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> E. r e. B ( w .+ r ) = a ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> E. r e. B ( w .+ r ) = a ) with typecode |- |
42 |
|
oveq2 |
|
43 |
42
|
eqeq1d |
|
44 |
43
|
cbvrexvw |
|
45 |
|
simpll1 |
Could not format ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) -> G e. Smgrp ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) -> G e. Smgrp ) with typecode |- |
46 |
45
|
adantr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> G e. Smgrp ) with typecode |- |
47 |
|
simplr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> u e. B ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> u e. B ) with typecode |- |
48 |
|
simpllr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> w e. B ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> w e. B ) with typecode |- |
49 |
|
simprr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> z e. B ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> z e. B ) with typecode |- |
50 |
1 2
|
sgrpass |
Could not format ( ( G e. Smgrp /\ ( u e. B /\ w e. B /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( u .+ ( w .+ z ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( u e. B /\ w e. B /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( u .+ ( w .+ z ) ) ) with typecode |- |
51 |
46 47 48 49 50
|
syl13anc |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( u .+ ( w .+ z ) ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( u .+ ( w .+ z ) ) ) with typecode |- |
52 |
|
simprl |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( u .+ w ) = w ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( u .+ w ) = w ) with typecode |- |
53 |
52
|
oveq1d |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( w .+ z ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( w .+ z ) ) with typecode |- |
54 |
51 53
|
eqtr3d |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( u .+ ( w .+ z ) ) = ( w .+ z ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( ( u .+ w ) = w /\ z e. B ) ) -> ( u .+ ( w .+ z ) ) = ( w .+ z ) ) with typecode |- |
55 |
54
|
anassrs |
Could not format ( ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) /\ z e. B ) -> ( u .+ ( w .+ z ) ) = ( w .+ z ) ) : No typesetting found for |- ( ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) /\ z e. B ) -> ( u .+ ( w .+ z ) ) = ( w .+ z ) ) with typecode |- |
56 |
|
oveq2 |
|
57 |
|
id |
|
58 |
56 57
|
eqeq12d |
|
59 |
55 58
|
syl5ibcom |
Could not format ( ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) /\ z e. B ) -> ( ( w .+ z ) = a -> ( u .+ a ) = a ) ) : No typesetting found for |- ( ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) /\ z e. B ) -> ( ( w .+ z ) = a -> ( u .+ a ) = a ) ) with typecode |- |
60 |
59
|
rexlimdva |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) -> ( E. z e. B ( w .+ z ) = a -> ( u .+ a ) = a ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) -> ( E. z e. B ( w .+ z ) = a -> ( u .+ a ) = a ) ) with typecode |- |
61 |
44 60
|
syl5bi |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) -> ( E. r e. B ( w .+ r ) = a -> ( u .+ a ) = a ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( u .+ w ) = w ) -> ( E. r e. B ( w .+ r ) = a -> ( u .+ a ) = a ) ) with typecode |- |
62 |
61
|
adantrl |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> ( E. r e. B ( w .+ r ) = a -> ( u .+ a ) = a ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> ( E. r e. B ( w .+ r ) = a -> ( u .+ a ) = a ) ) with typecode |- |
63 |
41 62
|
mpd |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> ( u .+ a ) = a ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> ( u .+ a ) = a ) with typecode |- |
64 |
|
oveq2 |
|
65 |
64
|
eqeq1d |
|
66 |
65
|
rexbidv |
|
67 |
|
oveq1 |
|
68 |
67
|
eqeq1d |
|
69 |
68
|
rexbidv |
|
70 |
66 69
|
anbi12d |
|
71 |
|
eqeq2 |
|
72 |
71
|
rexbidv |
|
73 |
|
eqeq2 |
|
74 |
73
|
rexbidv |
|
75 |
72 74
|
anbi12d |
|
76 |
70 75
|
rspc2va |
|
77 |
76
|
simpld |
|
78 |
77
|
ex |
|
79 |
78
|
ancoms |
|
80 |
79
|
com12 |
|
81 |
80
|
3ad2ant3 |
Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( u e. B /\ a e. B ) -> E. l e. B ( l .+ a ) = u ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( u e. B /\ a e. B ) -> E. l e. B ( l .+ a ) = u ) ) with typecode |- |
82 |
81
|
impl |
Could not format ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ u e. B ) /\ a e. B ) -> E. l e. B ( l .+ a ) = u ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ u e. B ) /\ a e. B ) -> E. l e. B ( l .+ a ) = u ) with typecode |- |
83 |
|
oveq1 |
|
84 |
83
|
eqeq1d |
|
85 |
84
|
cbvrexvw |
|
86 |
82 85
|
sylib |
Could not format ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ u e. B ) /\ a e. B ) -> E. i e. B ( i .+ a ) = u ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ u e. B ) /\ a e. B ) -> E. i e. B ( i .+ a ) = u ) with typecode |- |
87 |
86
|
adantllr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ a e. B ) -> E. i e. B ( i .+ a ) = u ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ a e. B ) -> E. i e. B ( i .+ a ) = u ) with typecode |- |
88 |
87
|
adantrr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> E. i e. B ( i .+ a ) = u ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> E. i e. B ( i .+ a ) = u ) with typecode |- |
89 |
63 88
|
jca |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ ( a e. B /\ ( u .+ w ) = w ) ) -> ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) with typecode |- |
90 |
89
|
expr |
Could not format ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ a e. B ) -> ( ( u .+ w ) = w -> ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) : No typesetting found for |- ( ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) /\ a e. B ) -> ( ( u .+ w ) = w -> ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) with typecode |- |
91 |
90
|
ralrimdva |
Could not format ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) -> ( ( u .+ w ) = w -> A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) /\ u e. B ) -> ( ( u .+ w ) = w -> A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) with typecode |- |
92 |
91
|
reximdva |
Could not format ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) -> ( E. u e. B ( u .+ w ) = w -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) -> ( E. u e. B ( u .+ w ) = w -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) with typecode |- |
93 |
30 92
|
mpd |
Could not format ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) /\ w e. B ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) with typecode |- |
94 |
5 93
|
exlimddv |
Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) with typecode |- |