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∈XuGx=x∧xGu=x∧∃y∈XyGx=u∧xGy=u

Proof

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