Metamath Proof Explorer


Theorem dfgrp3lem

Description: Lemma for dfgrp3 . (Contributed by AV, 28-Aug-2021)

Ref Expression
Hypotheses dfgrp3.b B = Base G
dfgrp3.p + ˙ = + G
Assertion dfgrp3lem Could not format assertion : 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 |-

Proof

Step Hyp Ref Expression
1 dfgrp3.b B = Base G
2 dfgrp3.p + ˙ = + G
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 B w w B
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 x = w l + ˙ x = l + ˙ w
7 6 eqeq1d x = w l + ˙ x = y l + ˙ w = y
8 7 rexbidv x = w l B l + ˙ x = y l B l + ˙ w = y
9 oveq1 x = w x + ˙ r = w + ˙ r
10 9 eqeq1d x = w x + ˙ r = y w + ˙ r = y
11 10 rexbidv x = w r B x + ˙ r = y r B w + ˙ r = y
12 8 11 anbi12d x = w l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ w = y r B w + ˙ r = y
13 12 ralbidv x = w y B l B l + ˙ x = y r B x + ˙ r = y y B l B l + ˙ w = y r B w + ˙ r = y
14 13 rspcv w B x B y B l B l + ˙ x = y r B x + ˙ r = y y B l B l + ˙ w = y r B w + ˙ r = y
15 eqeq2 y = w l + ˙ w = y l + ˙ w = w
16 15 rexbidv y = w l B l + ˙ w = y l B l + ˙ w = w
17 eqeq2 y = w w + ˙ r = y w + ˙ r = w
18 17 rexbidv y = w r B w + ˙ r = y r B w + ˙ r = w
19 16 18 anbi12d y = w l B l + ˙ w = y r B w + ˙ r = y l B l + ˙ w = w r B w + ˙ r = w
20 19 rspcva w B y B l B l + ˙ w = y r B w + ˙ r = y l B l + ˙ w = w r B w + ˙ r = w
21 oveq1 l = u l + ˙ w = u + ˙ w
22 21 eqeq1d l = u l + ˙ w = w u + ˙ w = w
23 22 cbvrexvw l B l + ˙ w = w u B u + ˙ w = w
24 23 biimpi l B l + ˙ w = w u B u + ˙ w = w
25 24 adantr l B l + ˙ w = w r B w + ˙ r = w u B u + ˙ w = w
26 20 25 syl w B y B l B l + ˙ w = y r B w + ˙ r = y u B u + ˙ w = w
27 26 ex w B y B l B l + ˙ w = y r B w + ˙ r = y u B u + ˙ w = w
28 14 27 syldc x B y B l B l + ˙ x = y r B x + ˙ r = y w B u B u + ˙ w = w
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 y = a l + ˙ w = y l + ˙ w = a
32 31 rexbidv y = a l B l + ˙ w = y l B l + ˙ w = a
33 eqeq2 y = a w + ˙ r = y w + ˙ r = a
34 33 rexbidv y = a r B w + ˙ r = y r B w + ˙ r = a
35 32 34 anbi12d y = a l B l + ˙ w = y r B w + ˙ r = y l B l + ˙ w = a r B w + ˙ r = a
36 12 35 rspc2va w B a B x B y B l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ w = a r B w + ˙ r = a
37 36 simprd w B a B x B y B l B l + ˙ x = y r B x + ˙ r = y r B w + ˙ r = a
38 37 expcom x B y B l B l + ˙ x = y r B x + ˙ r = y w B a B r B w + ˙ r = a
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 r = z w + ˙ r = w + ˙ z
43 42 eqeq1d r = z w + ˙ r = a w + ˙ z = a
44 43 cbvrexvw r B w + ˙ r = a z B w + ˙ z = a
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 w + ˙ z = a u + ˙ w + ˙ z = u + ˙ a
57 id w + ˙ z = a w + ˙ z = a
58 56 57 eqeq12d w + ˙ z = a u + ˙ w + ˙ z = w + ˙ z u + ˙ a = a
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 x = a l + ˙ x = l + ˙ a
65 64 eqeq1d x = a l + ˙ x = y l + ˙ a = y
66 65 rexbidv x = a l B l + ˙ x = y l B l + ˙ a = y
67 oveq1 x = a x + ˙ r = a + ˙ r
68 67 eqeq1d x = a x + ˙ r = y a + ˙ r = y
69 68 rexbidv x = a r B x + ˙ r = y r B a + ˙ r = y
70 66 69 anbi12d x = a l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ a = y r B a + ˙ r = y
71 eqeq2 y = u l + ˙ a = y l + ˙ a = u
72 71 rexbidv y = u l B l + ˙ a = y l B l + ˙ a = u
73 eqeq2 y = u a + ˙ r = y a + ˙ r = u
74 73 rexbidv y = u r B a + ˙ r = y r B a + ˙ r = u
75 72 74 anbi12d y = u l B l + ˙ a = y r B a + ˙ r = y l B l + ˙ a = u r B a + ˙ r = u
76 70 75 rspc2va a B u B x B y B l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ a = u r B a + ˙ r = u
77 76 simpld a B u B x B y B l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ a = u
78 77 ex a B u B x B y B l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ a = u
79 78 ancoms u B a B x B y B l B l + ˙ x = y r B x + ˙ r = y l B l + ˙ a = u
80 79 com12 x B y B l B l + ˙ x = y r B x + ˙ r = y u B a B l B l + ˙ a = u
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 l = i l + ˙ a = i + ˙ a
84 83 eqeq1d l = i l + ˙ a = u i + ˙ a = u
85 84 cbvrexvw l B l + ˙ a = u i B i + ˙ a = u
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 |-