Metamath Proof Explorer

Theorem grpinvid1

Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011)

Ref Expression
Hypotheses grpinv.b 
|- B = ( Base ` G )
grpinv.p 
|- .+ = ( +g ` G )
grpinv.u 
|- .0. = ( 0g ` G )
grpinv.n 
|- N = ( invg ` G )
Assertion grpinvid1 
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) = Y <-> ( X .+ Y ) = .0. ) )

Proof

Step Hyp Ref Expression
1 grpinv.b 
 |-  B = ( Base ` G )
2 grpinv.p 
 |-  .+ = ( +g ` G )
3 grpinv.u 
 |-  .0. = ( 0g ` G )
4 grpinv.n 
 |-  N = ( invg ` G )
5 oveq2 
 |-  ( ( N ` X ) = Y -> ( X .+ ( N ` X ) ) = ( X .+ Y ) )
6 5 adantl 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( N ` X ) = Y ) -> ( X .+ ( N ` X ) ) = ( X .+ Y ) )
7 1 2 3 4 grprinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( N ` X ) ) = .0. )
8 7 3adant3 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( N ` X ) ) = .0. )
9 8 adantr 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( N ` X ) = Y ) -> ( X .+ ( N ` X ) ) = .0. )
10 6 9 eqtr3d 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( N ` X ) = Y ) -> ( X .+ Y ) = .0. )
11 oveq2 
 |-  ( ( X .+ Y ) = .0. -> ( ( N ` X ) .+ ( X .+ Y ) ) = ( ( N ` X ) .+ .0. ) )
12 11 adantl 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( X .+ Y ) = .0. ) -> ( ( N ` X ) .+ ( X .+ Y ) ) = ( ( N ` X ) .+ .0. ) )
13 1 2 3 4 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )
14 13 oveq1d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( ( N ` X ) .+ X ) .+ Y ) = ( .0. .+ Y ) )
15 14 3adant3 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( ( N ` X ) .+ X ) .+ Y ) = ( .0. .+ Y ) )
16 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
17 16 adantrr 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B ) ) -> ( N ` X ) e. B )
18 simprl 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B ) ) -> X e. B )
19 simprr 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
20 17 18 19 3jca 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B ) ) -> ( ( N ` X ) e. B /\ X e. B /\ Y e. B ) )
21 1 2 grpass 
 |-  ( ( G e. Grp /\ ( ( N ` X ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( N ` X ) .+ X ) .+ Y ) = ( ( N ` X ) .+ ( X .+ Y ) ) )
22 20 21 syldan 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B ) ) -> ( ( ( N ` X ) .+ X ) .+ Y ) = ( ( N ` X ) .+ ( X .+ Y ) ) )
23 22 3impb 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( ( N ` X ) .+ X ) .+ Y ) = ( ( N ` X ) .+ ( X .+ Y ) ) )
24 15 23 eqtr3d 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( .0. .+ Y ) = ( ( N ` X ) .+ ( X .+ Y ) ) )
25 1 2 3 grplid 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( .0. .+ Y ) = Y )
26 25 3adant2 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( .0. .+ Y ) = Y )
27 24 26 eqtr3d 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) .+ ( X .+ Y ) ) = Y )
28 27 adantr 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( X .+ Y ) = .0. ) -> ( ( N ` X ) .+ ( X .+ Y ) ) = Y )
29 1 2 3 grprid 
 |-  ( ( G e. Grp /\ ( N ` X ) e. B ) -> ( ( N ` X ) .+ .0. ) = ( N ` X ) )
30 16 29 syldan 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ .0. ) = ( N ` X ) )
31 30 3adant3 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) .+ .0. ) = ( N ` X ) )
32 31 adantr 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( X .+ Y ) = .0. ) -> ( ( N ` X ) .+ .0. ) = ( N ` X ) )
33 12 28 32 3eqtr3rd 
 |-  ( ( ( G e. Grp /\ X e. B /\ Y e. B ) /\ ( X .+ Y ) = .0. ) -> ( N ` X ) = Y )
34 10 33 impbida 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) = Y <-> ( X .+ Y ) = .0. ) )