Metamath Proof Explorer

Theorem grpoidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 ⊢ X = ran ⁡ G
Assertion grpoidinv ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ X = ran ⁡ G
2 simpl ⊢ u G z = z ∧ ∃ w ∈ X w G z = u → u G z = z
3 2 ralimi ⊢ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → ∀ z ∈ X u G z = z
4 oveq2 ⊢ z = x → u G z = u G x
5 id ⊢ z = x → z = x
6 4 5 eqeq12d ⊢ z = x → u G z = z ↔ u G x = x
7 6 rspccva ⊢ ∀ z ∈ X u G z = z ∧ x ∈ X → u G x = x
8 3 7 sylan ⊢ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → u G x = x
9 8 adantll ⊢ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → u G x = x
10 9 adantll ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → u G x = x
11 simpl ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → G ∈ GrpOp
12 11 anim1i ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → G ∈ GrpOp ∧ x ∈ X
13 id ⊢ G ∈ GrpOp ∧ u ∈ X → G ∈ GrpOp ∧ u ∈ X
14 13 adantrr ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → G ∈ GrpOp ∧ u ∈ X
15 14 adantr ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → G ∈ GrpOp ∧ u ∈ X
16 3 adantl ⊢ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → ∀ z ∈ X u G z = z
17 16 ad2antlr ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → ∀ z ∈ X u G z = z
18 simpr ⊢ u G z = z ∧ ∃ w ∈ X w G z = u → ∃ w ∈ X w G z = u
19 18 ralimi ⊢ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → ∀ z ∈ X ∃ w ∈ X w G z = u
20 19 adantl ⊢ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → ∀ z ∈ X ∃ w ∈ X w G z = u
21 20 ad2antlr ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → ∀ z ∈ X ∃ w ∈ X w G z = u
22 15 17 21 jca32 ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∀ z ∈ X ∃ w ∈ X w G z = u
23 biid ⊢ ∀ z ∈ X u G z = z ↔ ∀ z ∈ X u G z = z
24 biid ⊢ ∀ z ∈ X ∃ w ∈ X w G z = u ↔ ∀ z ∈ X ∃ w ∈ X w G z = u
25 1 23 24 grpoidinvlem3 ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∀ z ∈ X ∃ w ∈ X w G z = u ∧ x ∈ X → ∃ y ∈ X y G x = u ∧ x G y = u
26 22 25 sylancom ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → ∃ y ∈ X y G x = u ∧ x G y = u
27 1 grpoidinvlem4 ⊢ G ∈ GrpOp ∧ x ∈ X ∧ ∃ y ∈ X y G x = u ∧ x G y = u → x G u = u G x
28 12 26 27 syl2anc ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → x G u = u G x
29 28 10 eqtrd ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → x G u = x
30 10 29 26 jca31 ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u ∧ x ∈ X → u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u
31 30 ralrimiva ⊢ G ∈ GrpOp ∧ u ∈ X ∧ ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u → ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u
32 1 grpolidinv ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ z ∈ X u G z = z ∧ ∃ w ∈ X w G z = u
33 31 32 reximddv ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u