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

Metamath Proof Explorer

Theorem lidrididd

Description: If there is a left and right identity element for any binary operation (group operation) .+ , the left identity element (and therefore also the right identity element according to lidrideqd ) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023)

Ref Expression
Hypotheses lidrideqd.l 
|- ( ph -> L e. B )
lidrideqd.r 
|- ( ph -> R e. B )
lidrideqd.li 
|- ( ph -> A. x e. B ( L .+ x ) = x )
lidrideqd.ri 
|- ( ph -> A. x e. B ( x .+ R ) = x )
lidrideqd.b 
|- B = ( Base ` G )
lidrideqd.p 
|- .+ = ( +g ` G )
lidrididd.o 
|- .0. = ( 0g ` G )
Assertion lidrididd 
|- ( ph -> L = .0. )

Proof

Step Hyp Ref Expression
1 lidrideqd.l 
 |-  ( ph -> L e. B )
2 lidrideqd.r 
 |-  ( ph -> R e. B )
3 lidrideqd.li 
 |-  ( ph -> A. x e. B ( L .+ x ) = x )
4 lidrideqd.ri 
 |-  ( ph -> A. x e. B ( x .+ R ) = x )
5 lidrideqd.b 
 |-  B = ( Base ` G )
6 lidrideqd.p 
 |-  .+ = ( +g ` G )
7 lidrididd.o 
 |-  .0. = ( 0g ` G )
8 oveq2 
 |-  ( x = y -> ( L .+ x ) = ( L .+ y ) )
9 id 
 |-  ( x = y -> x = y )
10 8 9 eqeq12d 
 |-  ( x = y -> ( ( L .+ x ) = x <-> ( L .+ y ) = y ) )
11 10 rspcv 
 |-  ( y e. B -> ( A. x e. B ( L .+ x ) = x -> ( L .+ y ) = y ) )
12 3 11 mpan9 
 |-  ( ( ph /\ y e. B ) -> ( L .+ y ) = y )
13 1 2 3 4 lidrideqd 
 |-  ( ph -> L = R )
14 oveq1 
 |-  ( x = y -> ( x .+ R ) = ( y .+ R ) )
15 14 9 eqeq12d 
 |-  ( x = y -> ( ( x .+ R ) = x <-> ( y .+ R ) = y ) )
16 15 rspcv 
 |-  ( y e. B -> ( A. x e. B ( x .+ R ) = x -> ( y .+ R ) = y ) )
17 oveq2 
 |-  ( L = R -> ( y .+ L ) = ( y .+ R ) )
18 17 adantl 
 |-  ( ( ( y .+ R ) = y /\ L = R ) -> ( y .+ L ) = ( y .+ R ) )
19 simpl 
 |-  ( ( ( y .+ R ) = y /\ L = R ) -> ( y .+ R ) = y )
20 18 19 eqtrd 
 |-  ( ( ( y .+ R ) = y /\ L = R ) -> ( y .+ L ) = y )
21 20 ex 
 |-  ( ( y .+ R ) = y -> ( L = R -> ( y .+ L ) = y ) )
22 16 21 syl6com 
 |-  ( A. x e. B ( x .+ R ) = x -> ( y e. B -> ( L = R -> ( y .+ L ) = y ) ) )
23 22 com23 
 |-  ( A. x e. B ( x .+ R ) = x -> ( L = R -> ( y e. B -> ( y .+ L ) = y ) ) )
24 4 13 23 sylc 
 |-  ( ph -> ( y e. B -> ( y .+ L ) = y ) )
25 24 imp 
 |-  ( ( ph /\ y e. B ) -> ( y .+ L ) = y )
26 5 7 6 1 12 25 ismgmid2 
 |-  ( ph -> L = .0. )