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 ` G )
Assertion dfgrp3lem 
|- ( ( 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 ) )

Proof

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