Metamath Proof Explorer

Theorem grpomndo

Description: A group is a monoid. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion grpomndo ⊢G∈GrpOp→G∈MndOp

Proof

Step Hyp Ref Expression
1 eqid ⊢ran⁡G=ran⁡G
2 1 isgrpo ⊢G∈GrpOp→G∈GrpOp↔G:ran⁡G×ran⁡G⟶ran⁡G∧∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧∃w∈ran⁡G∀x∈ran⁡GwGx=x∧∃y∈ran⁡GyGx=w
3 2 biimpd ⊢G∈GrpOp→G∈GrpOp→G:ran⁡G×ran⁡G⟶ran⁡G∧∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧∃w∈ran⁡G∀x∈ran⁡GwGx=x∧∃y∈ran⁡GyGx=w
4 1 grpoidinv ⊢G∈GrpOp→∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y∧∃w∈ran⁡GwGy=x∧yGw=x
5 simpl ⊢xGy=y∧yGx=y∧∃w∈ran⁡GwGy=x∧yGw=x→xGy=y∧yGx=y
6 5 ralimi ⊢∀y∈ran⁡GxGy=y∧yGx=y∧∃w∈ran⁡GwGy=x∧yGw=x→∀y∈ran⁡GxGy=y∧yGx=y
7 6 reximi ⊢∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y∧∃w∈ran⁡GwGy=x∧yGw=x→∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y
8 1 ismndo2 ⊢G∈GrpOp→G∈MndOp↔G:ran⁡G×ran⁡G⟶ran⁡G∧∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y
9 8 biimprcd ⊢G:ran⁡G×ran⁡G⟶ran⁡G∧∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y→G∈GrpOp→G∈MndOp
10 9 3exp ⊢G:ran⁡G×ran⁡G⟶ran⁡G→∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz→∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y→G∈GrpOp→G∈MndOp
11 10 impcom ⊢∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧G:ran⁡G×ran⁡G⟶ran⁡G→∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y→G∈GrpOp→G∈MndOp
12 11 com3l ⊢∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧G:ran⁡G×ran⁡G⟶ran⁡G→G∈MndOp
13 7 12 syl ⊢∃x∈ran⁡G∀y∈ran⁡GxGy=y∧yGx=y∧∃w∈ran⁡GwGy=x∧yGw=x→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧G:ran⁡G×ran⁡G⟶ran⁡G→G∈MndOp
14 4 13 mpcom ⊢G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧G:ran⁡G×ran⁡G⟶ran⁡G→G∈MndOp
15 14 expdcom ⊢∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz→G:ran⁡G×ran⁡G⟶ran⁡G→G∈GrpOp→G∈MndOp
16 15 a1i ⊢∃w∈ran⁡G∀x∈ran⁡GwGx=x∧∃y∈ran⁡GyGx=w→∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz→G:ran⁡G×ran⁡G⟶ran⁡G→G∈GrpOp→G∈MndOp
17 16 com13 ⊢G:ran⁡G×ran⁡G⟶ran⁡G→∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz→∃w∈ran⁡G∀x∈ran⁡GwGx=x∧∃y∈ran⁡GyGx=w→G∈GrpOp→G∈MndOp
18 17 3imp ⊢G:ran⁡G×ran⁡G⟶ran⁡G∧∀x∈ran⁡G∀y∈ran⁡G∀z∈ran⁡GxGyGz=xGyGz∧∃w∈ran⁡G∀x∈ran⁡GwGx=x∧∃y∈ran⁡GyGx=w→G∈GrpOp→G∈MndOp
19 3 18 syli ⊢G∈GrpOp→G∈GrpOp→G∈MndOp
20 19 pm2.43i ⊢G∈GrpOp→G∈MndOp