This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by AV, 1-Sep-2021)

Ref Expression
Hypotheses grplrinv.b 
|- B = ( Base ` G )
grplrinv.p 
|- .+ = ( +g ` G )
grplrinv.i 
|- .0. = ( 0g ` G )
Assertion grpidinv2 
|- ( ( G e. Grp /\ A e. B ) -> ( ( ( .0. .+ A ) = A /\ ( A .+ .0. ) = A ) /\ E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 grplrinv.b 
 |-  B = ( Base ` G )
2 grplrinv.p 
 |-  .+ = ( +g ` G )
3 grplrinv.i 
 |-  .0. = ( 0g ` G )
4 1 2 3 grplid 
 |-  ( ( G e. Grp /\ A e. B ) -> ( .0. .+ A ) = A )
5 1 2 3 grprid 
 |-  ( ( G e. Grp /\ A e. B ) -> ( A .+ .0. ) = A )
6 1 2 3 grplrinv 
 |-  ( G e. Grp -> A. z e. B E. y e. B ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) )
7 oveq2 
 |-  ( z = A -> ( y .+ z ) = ( y .+ A ) )
8 7 eqeq1d 
 |-  ( z = A -> ( ( y .+ z ) = .0. <-> ( y .+ A ) = .0. ) )
9 oveq1 
 |-  ( z = A -> ( z .+ y ) = ( A .+ y ) )
10 9 eqeq1d 
 |-  ( z = A -> ( ( z .+ y ) = .0. <-> ( A .+ y ) = .0. ) )
11 8 10 anbi12d 
 |-  ( z = A -> ( ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) <-> ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
12 11 rexbidv 
 |-  ( z = A -> ( E. y e. B ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) <-> E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
13 12 rspcv 
 |-  ( A e. B -> ( A. z e. B E. y e. B ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) -> E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
14 6 13 mpan9 
 |-  ( ( G e. Grp /\ A e. B ) -> E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) )
15 4 5 14 jca31 
 |-  ( ( G e. Grp /\ A e. B ) -> ( ( ( .0. .+ A ) = A /\ ( A .+ .0. ) = A ) /\ E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )