# 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 )`
` |-  ( ( ( ph /\ ps ) /\ A e. X ) -> E. y e. X ( y G A ) = U )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ A e. X ) /\ y e. X ) -> ( A G y ) e. X )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) -> A. x e. X ( U G x ) = x )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ A e. X ) /\ y e. X ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )`
` |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( G e. GrpOp /\ ( y e. X /\ A e. X ) ) )`
` |-  ( ( ( ( ( ( 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 )`
` |-  ( ( ( ph /\ ps ) /\ y e. X ) -> ( U G y ) = y )`
` |-  ( ( ( ( ph /\ ps ) /\ A e. X ) /\ y e. X ) -> ( U G y ) = y )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( U G ( A G y ) ) = U )`
` |-  ( ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( A G y ) = U )`
` |-  ( ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U -> ( A G y ) = U ) )`
` |-  ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ U e. X ) /\ ( ph /\ ps ) ) /\ A e. X ) -> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) )`