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 biimpi 
 |-  ( E. l e. B ( l .+ w ) = w -> E. u e. B ( u .+ w ) = w )
25 24 adantr 
 |-  ( ( E. l e. B ( l .+ w ) = w /\ E. r e. B ( w .+ r ) = w ) -> E. u e. B ( u .+ w ) = w )
26 20 25 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 )
27 26 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 ) )
28 14 27 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 ) )
29 28 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 ) )
30 29 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 )
31 eqeq2 
 |-  ( y = a -> ( ( l .+ w ) = y <-> ( l .+ w ) = a ) )
32 31 rexbidv 
 |-  ( y = a -> ( E. l e. B ( l .+ w ) = y <-> E. l e. B ( l .+ w ) = a ) )
33 eqeq2 
 |-  ( y = a -> ( ( w .+ r ) = y <-> ( w .+ r ) = a ) )
34 33 rexbidv 
 |-  ( y = a -> ( E. r e. B ( w .+ r ) = y <-> E. r e. B ( w .+ r ) = a ) )
35 32 34 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 ) ) )
36 12 35 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 ) )
37 36 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 )
38 37 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 ) )
39 38 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 ) )
40 39 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 )
41 40 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 )
42 oveq2 
 |-  ( r = z -> ( w .+ r ) = ( w .+ z ) )
43 42 eqeq1d 
 |-  ( r = z -> ( ( w .+ r ) = a <-> ( w .+ z ) = a ) )
44 43 cbvrexvw 
 |-  ( E. r e. B ( w .+ r ) = a <-> E. z e. B ( w .+ z ) = a )
45 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 )
46 45 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 )
47 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 )
48 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 )
49 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 )
50 1 2 sgrpass 
 |-  ( ( G e. Smgrp /\ ( u e. B /\ w e. B /\ z e. B ) ) -> ( ( u .+ w ) .+ z ) = ( u .+ ( w .+ z ) ) )
51 46 47 48 49 50 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 ) ) )
52 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 )
53 52 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 ) )
54 51 53 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 ) )
55 54 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 ) )
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 
 |-  ( ( ( ( ( ( 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 ) )
60 59 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 ) )
61 44 60 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 ) )
62 61 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 ) )
63 41 62 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 )
64 oveq2 
 |-  ( x = a -> ( l .+ x ) = ( l .+ a ) )
65 64 eqeq1d 
 |-  ( x = a -> ( ( l .+ x ) = y <-> ( l .+ a ) = y ) )
66 65 rexbidv 
 |-  ( x = a -> ( E. l e. B ( l .+ x ) = y <-> E. l e. 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 -> ( E. r e. B ( x .+ r ) = y <-> E. r e. B ( a .+ r ) = y ) )
70 66 69 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 ) ) )
71 eqeq2 
 |-  ( y = u -> ( ( l .+ a ) = y <-> ( l .+ a ) = u ) )
72 71 rexbidv 
 |-  ( y = u -> ( E. l e. B ( l .+ a ) = y <-> E. l e. B ( l .+ a ) = u ) )
73 eqeq2 
 |-  ( y = u -> ( ( a .+ r ) = y <-> ( a .+ r ) = u ) )
74 73 rexbidv 
 |-  ( y = u -> ( E. r e. B ( a .+ r ) = y <-> E. r e. B ( a .+ r ) = u ) )
75 72 74 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 ) ) )
76 70 75 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 ) )
77 76 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 )
78 77 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 ) )
79 78 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 ) )
80 79 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 ) )
81 80 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 ) )
82 81 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 )
83 oveq1 
 |-  ( l = i -> ( l .+ a ) = ( i .+ a ) )
84 83 eqeq1d 
 |-  ( l = i -> ( ( l .+ a ) = u <-> ( i .+ a ) = u ) )
85 84 cbvrexvw 
 |-  ( E. l e. B ( l .+ a ) = u <-> E. i e. B ( i .+ a ) = u )
86 82 85 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 )
87 86 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 )
88 87 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 )
89 63 88 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 ) )
90 89 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 ) ) )
91 90 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 ) ) )
92 91 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 ) ) )
93 30 92 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 ) )
94 5 93 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 ) )