Theorem dfgrp3lem

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

	Ref	Expression
Hypotheses	dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
	dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_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={\mathrm{Base}}_G$$
2		dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_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\ne \varnothing \leftrightarrow \exists ww\in 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\to l\underset{\dot{}}{+}x=l\underset{\dot{}}{+}w$$
7	6	eqeq1d	$$⊢x=w\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow l\underset{\dot{}}{+}w=y\right)$$
8	7	rexbidv	$$⊢x=w\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=y\right)$$
9		oveq1	$$⊢x=w\to x\underset{\dot{}}{+}r=w\underset{\dot{}}{+}r$$
10	9	eqeq1d	$$⊢x=w\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=y\right)$$
11	10	rexbidv	$$⊢x=w\to \left(\exists r\in Bx\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=y\right)$$
12	8 11	anbi12d	$$⊢x=w\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)$$
13	12	ralbidv	$$⊢x=w\to \left(\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\leftrightarrow \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)$$
14	13	rspcv	$$⊢w\in B\to \left(\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)$$
15		eqeq2	$$⊢y=w\to \left(l\underset{\dot{}}{+}w=y\leftrightarrow l\underset{\dot{}}{+}w=w\right)$$
16	15	rexbidv	$$⊢y=w\to \left(\exists l\in Bl\underset{\dot{}}{+}w=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=w\right)$$
17		eqeq2	$$⊢y=w\to \left(w\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=w\right)$$
18	17	rexbidv	$$⊢y=w\to \left(\exists r\in Bw\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=w\right)$$
19	16 18	anbi12d	$$⊢y=w\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}w=w\wedge \exists r\in Bw\underset{\dot{}}{+}r=w\right)\right)$$
20	19	rspcva	$$⊢\left(w\in B\wedge \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}w=w\wedge \exists r\in Bw\underset{\dot{}}{+}r=w\right)$$
21		oveq1	$$⊢l=u\to l\underset{\dot{}}{+}w=u\underset{\dot{}}{+}w$$
22	21	eqeq1d	$$⊢l=u\to \left(l\underset{\dot{}}{+}w=w\leftrightarrow u\underset{\dot{}}{+}w=w\right)$$
23	22	cbvrexvw	$$⊢\exists l\in Bl\underset{\dot{}}{+}w=w\leftrightarrow \exists u\in Bu\underset{\dot{}}{+}w=w$$
24	23	biimpi	$$⊢\exists l\in Bl\underset{\dot{}}{+}w=w\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
25	24	adantr	$$⊢\left(\exists l\in Bl\underset{\dot{}}{+}w=w\wedge \exists r\in Bw\underset{\dot{}}{+}r=w\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
26	20 25	syl	$$⊢\left(w\in B\wedge \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
27	26	ex	$$⊢w\in B\to \left(\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w\right)$$
28	14 27	syldc	$$⊢\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \left(w\in B\to \exists u\in Bu\underset{\dot{}}{+}w=w\right)$$
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\to \left(l\underset{\dot{}}{+}w=y\leftrightarrow l\underset{\dot{}}{+}w=a\right)$$
32	31	rexbidv	$$⊢y=a\to \left(\exists l\in Bl\underset{\dot{}}{+}w=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=a\right)$$
33		eqeq2	$$⊢y=a\to \left(w\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=a\right)$$
34	33	rexbidv	$$⊢y=a\to \left(\exists r\in Bw\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
35	32 34	anbi12d	$$⊢y=a\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}w=a\wedge \exists r\in Bw\underset{\dot{}}{+}r=a\right)\right)$$
36	12 35	rspc2va	$$⊢\left(\left(w\in B\wedge a\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}w=a\wedge \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
37	36	simprd	$$⊢\left(\left(w\in B\wedge a\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a$$
38	37	expcom	$$⊢\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \left(\left(w\in B\wedge a\in B\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
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\to w\underset{\dot{}}{+}r=w\underset{\dot{}}{+}z$$
43	42	eqeq1d	$$⊢r=z\to \left(w\underset{\dot{}}{+}r=a\leftrightarrow w\underset{\dot{}}{+}z=a\right)$$
44	43	cbvrexvw	$$⊢\exists r\in Bw\underset{\dot{}}{+}r=a\leftrightarrow \exists z\in Bw\underset{\dot{}}{+}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\underset{\dot{}}{+}z=a\to u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=u\underset{\dot{}}{+}a$$
57		id	$$⊢w\underset{\dot{}}{+}z=a\to w\underset{\dot{}}{+}z=a$$
58	56 57	eqeq12d	$$⊢w\underset{\dot{}}{+}z=a\to \left(u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=w\underset{\dot{}}{+}z\leftrightarrow u\underset{\dot{}}{+}a=a\right)$$
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\to l\underset{\dot{}}{+}x=l\underset{\dot{}}{+}a$$
65	64	eqeq1d	$$⊢x=a\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow l\underset{\dot{}}{+}a=y\right)$$
66	65	rexbidv	$$⊢x=a\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}a=y\right)$$
67		oveq1	$$⊢x=a\to x\underset{\dot{}}{+}r=a\underset{\dot{}}{+}r$$
68	67	eqeq1d	$$⊢x=a\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow a\underset{\dot{}}{+}r=y\right)$$
69	68	rexbidv	$$⊢x=a\to \left(\exists r\in Bx\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Ba\underset{\dot{}}{+}r=y\right)$$
70	66 69	anbi12d	$$⊢x=a\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}a=y\wedge \exists r\in Ba\underset{\dot{}}{+}r=y\right)\right)$$
71		eqeq2	$$⊢y=u\to \left(l\underset{\dot{}}{+}a=y\leftrightarrow l\underset{\dot{}}{+}a=u\right)$$
72	71	rexbidv	$$⊢y=u\to \left(\exists l\in Bl\underset{\dot{}}{+}a=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
73		eqeq2	$$⊢y=u\to \left(a\underset{\dot{}}{+}r=y\leftrightarrow a\underset{\dot{}}{+}r=u\right)$$
74	73	rexbidv	$$⊢y=u\to \left(\exists r\in Ba\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Ba\underset{\dot{}}{+}r=u\right)$$
75	72 74	anbi12d	$$⊢y=u\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}a=y\wedge \exists r\in Ba\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}a=u\wedge \exists r\in Ba\underset{\dot{}}{+}r=u\right)\right)$$
76	70 75	rspc2va	$$⊢\left(\left(a\in B\wedge u\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}a=u\wedge \exists r\in Ba\underset{\dot{}}{+}r=u\right)$$
77	76	simpld	$$⊢\left(\left(a\in B\wedge u\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u$$
78	77	ex	$$⊢\left(a\in B\wedge u\in B\right)\to \left(\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
79	78	ancoms	$$⊢\left(u\in B\wedge a\in B\right)\to \left(\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
80	79	com12	$$⊢\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \left(\left(u\in B\wedge a\in B\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
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\to l\underset{\dot{}}{+}a=i\underset{\dot{}}{+}a$$
84	83	eqeq1d	$$⊢l=i\to \left(l\underset{\dot{}}{+}a=u\leftrightarrow i\underset{\dot{}}{+}a=u\right)$$
85	84	cbvrexvw	$$⊢\exists l\in Bl\underset{\dot{}}{+}a=u\leftrightarrow \exists i\in Bi\underset{\dot{}}{+}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 |-