Metamath Proof Explorer

Theorem grpoidinvlem3

Description: Lemma for grpoidinv . (Contributed by NM, 11-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpfo.1 
|- X = ran G
grpidinvlem3.2 
|- ( ph <-> A. x e. X ( U G x ) = x )
grpidinvlem3.3 
|- ( ps <-> A. x e. X E. z e. X ( z G x ) = U )
Assertion grpoidinvlem3 
|- ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) -> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) )

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 grpidinvlem3.2 
 |-  ( ph <-> A. x e. X ( U G x ) = x )
3 grpidinvlem3.3 
 |-  ( ps <-> A. x e. X E. z e. X ( z G x ) = U )
4 oveq1 
 |-  ( z = y -> ( z G x ) = ( y G x ) )
5 4 eqeq1d 
 |-  ( z = y -> ( ( z G x ) = U <-> ( y G x ) = U ) )
6 5 cbvrexvw 
 |-  ( E. z e. X ( z G x ) = U <-> E. y e. X ( y G x ) = U )
7 6 ralbii 
 |-  ( A. x e. X E. z e. X ( z G x ) = U <-> A. x e. X E. y e. X ( y G x ) = U )
8 3 7 bitri 
 |-  ( ps <-> A. x e. X E. y e. X ( y G x ) = U )
9 oveq2 
 |-  ( x = A -> ( y G x ) = ( y G A ) )
10 9 eqeq1d 
 |-  ( x = A -> ( ( y G x ) = U <-> ( y G A ) = U ) )
11 10 rexbidv 
 |-  ( x = A -> ( E. y e. X ( y G x ) = U <-> E. y e. X ( y G A ) = U ) )
12 11 rspccva 
 |-  ( ( A. x e. X E. y e. X ( y G x ) = U /\ A e. X ) -> E. y e. X ( y G A ) = U )
13 8 12 sylanb 
 |-  ( ( ps /\ A e. X ) -> E. y e. X ( y G A ) = U )
14 13 adantll 
 |-  ( ( ( ph /\ ps ) /\ A e. X ) -> E. y e. X ( y G A ) = U )
15 14 adantll 
 |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) -> E. y e. X ( y G A ) = U )
16 1 grpocl 
 |-  ( ( G e. GrpOp /\ A e. X /\ y e. X ) -> ( A G y ) e. X )
17 16 3expa 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( A G y ) e. X )
18 17 adantllr 
 |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ A e. X ) /\ y e. X ) -> ( A G y ) e. X )
19 18 adantllr 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( A G y ) e. X )
20 2 biimpi 
 |-  ( ph -> A. x e. X ( U G x ) = x )
21 20 ad2antrl 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) -> A. x e. X ( U G x ) = x )
22 21 ad2antrr 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> A. x e. X ( U G x ) = x )
23 oveq2 
 |-  ( x = ( A G y ) -> ( U G x ) = ( U G ( A G y ) ) )
24 id 
 |-  ( x = ( A G y ) -> x = ( A G y ) )
25 23 24 eqeq12d 
 |-  ( x = ( A G y ) -> ( ( U G x ) = x <-> ( U G ( A G y ) ) = ( A G y ) ) )
26 25 rspcva 
 |-  ( ( ( A G y ) e. X /\ A. x e. X ( U G x ) = x ) -> ( U G ( A G y ) ) = ( A G y ) )
27 19 22 26 syl2anc 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( U G ( A G y ) ) = ( A G y ) )
28 27 adantr 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( U G ( A G y ) ) = ( A G y ) )
29 pm3.22 
 |-  ( ( ( y e. X /\ A e. X ) /\ G e. GrpOp ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )
30 29 an31s 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )
31 30 adantllr 
 |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ A e. X ) /\ y e. X ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )
32 31 adantllr 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )
33 32 adantr 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )
34 oveq2 
 |-  ( x = y -> ( U G x ) = ( U G y ) )
35 id 
 |-  ( x = y -> x = y )
36 34 35 eqeq12d 
 |-  ( x = y -> ( ( U G x ) = x <-> ( U G y ) = y ) )
37 36 rspccva 
 |-  ( ( A. x e. X ( U G x ) = x /\ y e. X ) -> ( U G y ) = y )
38 2 37 sylanb 
 |-  ( ( ph /\ y e. X ) -> ( U G y ) = y )
39 38 adantlr 
 |-  ( ( ( ph /\ ps ) /\ y e. X ) -> ( U G y ) = y )
40 39 adantlr 
 |-  ( ( ( ( ph /\ ps ) /\ A e. X ) /\ y e. X ) -> ( U G y ) = y )
41 40 adantlll 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( U G y ) = y )
42 41 anim1i 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( ( U G y ) = y /\ ( y G A ) = U ) )
43 1 grpoidinvlem2 
 |-  ( ( ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) /\ ( ( U G y ) = y /\ ( y G A ) = U ) ) -> ( ( A G y ) G ( A G y ) ) = ( A G y ) )
44 33 42 43 syl2anc 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( ( A G y ) G ( A G y ) ) = ( A G y ) )
45 16 3expb 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ y e. X ) ) -> ( A G y ) e. X )
46 45 ad2ant2rl 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) -> ( A G y ) e. X )
47 oveq1 
 |-  ( z = w -> ( z G x ) = ( w G x ) )
48 47 eqeq1d 
 |-  ( z = w -> ( ( z G x ) = U <-> ( w G x ) = U ) )
49 48 cbvrexvw 
 |-  ( E. z e. X ( z G x ) = U <-> E. w e. X ( w G x ) = U )
50 49 ralbii 
 |-  ( A. x e. X E. z e. X ( z G x ) = U <-> A. x e. X E. w e. X ( w G x ) = U )
51 3 50 bitri 
 |-  ( ps <-> A. x e. X E. w e. X ( w G x ) = U )
52 oveq2 
 |-  ( x = ( A G y ) -> ( w G x ) = ( w G ( A G y ) ) )
53 52 eqeq1d 
 |-  ( x = ( A G y ) -> ( ( w G x ) = U <-> ( w G ( A G y ) ) = U ) )
54 53 rexbidv 
 |-  ( x = ( A G y ) -> ( E. w e. X ( w G x ) = U <-> E. w e. X ( w G ( A G y ) ) = U ) )
55 54 rspcva 
 |-  ( ( ( A G y ) e. X /\ A. x e. X E. w e. X ( w G x ) = U ) -> E. w e. X ( w G ( A G y ) ) = U )
56 51 55 sylan2b 
 |-  ( ( ( A G y ) e. X /\ ps ) -> E. w e. X ( w G ( A G y ) ) = U )
57 anass 
 |-  ( ( ( G e. GrpOp /\ w e. X ) /\ ( A G y ) e. X ) <-> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) )
58 57 biimpi 
 |-  ( ( ( G e. GrpOp /\ w e. X ) /\ ( A G y ) e. X ) -> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) )
59 58 an32s 
 |-  ( ( ( G e. GrpOp /\ ( A G y ) e. X ) /\ w e. X ) -> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) )
60 59 ex 
 |-  ( ( G e. GrpOp /\ ( A G y ) e. X ) -> ( w e. X -> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) ) )
61 45 60 syldan 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ y e. X ) ) -> ( w e. X -> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) ) )
62 61 ad2ant2rl 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) -> ( w e. X -> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) ) )
63 62 imp 
 |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) /\ w e. X ) -> ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) )
64 1 grpoidinvlem1 
 |-  ( ( ( G e. GrpOp /\ ( w e. X /\ ( A G y ) e. X ) ) /\ ( ( w G ( A G y ) ) = U /\ ( ( A G y ) G ( A G y ) ) = ( A G y ) ) ) -> ( U G ( A G y ) ) = U )
65 63 64 sylan 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) /\ w e. X ) /\ ( ( w G ( A G y ) ) = U /\ ( ( A G y ) G ( A G y ) ) = ( A G y ) ) ) -> ( U G ( A G y ) ) = U )
66 65 exp43 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) -> ( w e. X -> ( ( w G ( A G y ) ) = U -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) ) )
67 66 rexlimdv 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) -> ( E. w e. X ( w G ( A G y ) ) = U -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) )
68 56 67 syl5 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) -> ( ( ( A G y ) e. X /\ ps ) -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) )
69 46 68 mpand 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ( A e. X /\ y e. X ) ) ) -> ( ps -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) )
70 69 exp32 
 |-  ( ( G e. GrpOp /\ U e. X ) -> ( ph -> ( ( A e. X /\ y e. X ) -> ( ps -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) ) ) )
71 70 com34 
 |-  ( ( G e. GrpOp /\ U e. X ) -> ( ph -> ( ps -> ( ( A e. X /\ y e. X ) -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) ) ) )
72 71 imp32 
 |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) -> ( ( A e. X /\ y e. X ) -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) ) )
73 72 impl 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) )
74 73 adantr 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( ( ( A G y ) G ( A G y ) ) = ( A G y ) -> ( U G ( A G y ) ) = U ) )
75 44 74 mpd 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( U G ( A G y ) ) = U )
76 28 75 eqtr3d 
 |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( A G y ) = U )
77 76 ex 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U -> ( A G y ) = U ) )
78 77 ancld 
 |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U -> ( ( y G A ) = U /\ ( A G y ) = U ) ) )
79 78 reximdva 
 |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) -> ( E. y e. X ( y G A ) = U -> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )
80 15 79 mpd 
 |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) -> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) )