Theorem grpoinv

Description: The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinv.1	|- X = ran G
	grpinv.2	|- U = ( GId ` G )
	grpinv.3	|- N = ( inv ` G )
Assertion	grpoinv	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) )

Proof

Step	Hyp	Ref	Expression
1		grpinv.1	|- X = ran G
2		grpinv.2	|- U = ( GId ` G )
3		grpinv.3	|- N = ( inv ` G )
4	1 2 3	grpoinvval	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) = ( iota_ y e. X ( y G A ) = U ) )
5	1 2	grpoinveu	|- ( ( G e. GrpOp /\ A e. X ) -> E! y e. X ( y G A ) = U )
6		riotacl2	|- ( E! y e. X ( y G A ) = U -> ( iota_ y e. X ( y G A ) = U ) e. { y e. X | ( y G A ) = U } )
7	5 6	syl	|- ( ( G e. GrpOp /\ A e. X ) -> ( iota_ y e. X ( y G A ) = U ) e. { y e. X | ( y G A ) = U } )
8	4 7	eqeltrd	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. { y e. X | ( y G A ) = U } )
9		simpl	|- ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U )
10	9	rgenw	|- A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U )
11	10	a1i	|- ( ( G e. GrpOp /\ A e. X ) -> A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U ) )
12	1 2	grpoidinv2	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )
13	12	simprd	|- ( ( G e. GrpOp /\ A e. X ) -> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) )
14	11 13 5	3jca	|- ( ( G e. GrpOp /\ A e. X ) -> ( A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) /\ E! y e. X ( y G A ) = U ) )
15		reupick2	|- ( ( ( A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) /\ E! y e. X ( y G A ) = U ) /\ y e. X ) -> ( ( y G A ) = U <-> ( ( y G A ) = U /\ ( A G y ) = U ) ) )
16	14 15	sylan	|- ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U <-> ( ( y G A ) = U /\ ( A G y ) = U ) ) )
17	16	rabbidva	|- ( ( G e. GrpOp /\ A e. X ) -> { y e. X | ( y G A ) = U } = { y e. X | ( ( y G A ) = U /\ ( A G y ) = U ) } )
18	8 17	eleqtrd	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. { y e. X | ( ( y G A ) = U /\ ( A G y ) = U ) } )
19		oveq1	|- ( y = ( N ` A ) -> ( y G A ) = ( ( N ` A ) G A ) )
20	19	eqeq1d	|- ( y = ( N ` A ) -> ( ( y G A ) = U <-> ( ( N ` A ) G A ) = U ) )
21		oveq2	|- ( y = ( N ` A ) -> ( A G y ) = ( A G ( N ` A ) ) )
22	21	eqeq1d	|- ( y = ( N ` A ) -> ( ( A G y ) = U <-> ( A G ( N ` A ) ) = U ) )
23	20 22	anbi12d	|- ( y = ( N ` A ) -> ( ( ( y G A ) = U /\ ( A G y ) = U ) <-> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) ) )
24	23	elrab	|- ( ( N ` A ) e. { y e. X | ( ( y G A ) = U /\ ( A G y ) = U ) } <-> ( ( N ` A ) e. X /\ ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) ) )
25	18 24	sylib	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) e. X /\ ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) ) )
26	25	simprd	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) )