**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 | ⊢ ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eqid | ⊢ ran 𝐺 = ran 𝐺 | |

2 | 1 | isgrpo | ⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑤 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑤 ) ) ) ) |

3 | 2 | biimpd | ⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 ∈ GrpOp → ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑤 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑤 ) ) ) ) |

4 | 1 | grpoidinv | ⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ∧ ∃ 𝑤 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑦 ) = 𝑥 ∧ ( 𝑦 𝐺 𝑤 ) = 𝑥 ) ) ) |

5 | simpl | ⊢ ( ( ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ∧ ∃ 𝑤 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑦 ) = 𝑥 ∧ ( 𝑦 𝐺 𝑤 ) = 𝑥 ) ) → ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) | |

6 | 5 | ralimi | ⊢ ( ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ∧ ∃ 𝑤 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑦 ) = 𝑥 ∧ ( 𝑦 𝐺 𝑤 ) = 𝑥 ) ) → ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) |

7 | 6 | reximi | ⊢ ( ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ∧ ∃ 𝑤 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑦 ) = 𝑥 ∧ ( 𝑦 𝐺 𝑤 ) = 𝑥 ) ) → ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) |

8 | 1 | ismndo2 | ⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) ) |

9 | 8 | biimprcd | ⊢ ( ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) |

10 | 9 | 3exp | ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) → ( ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) ) ) |

11 | 10 | impcom | ⊢ ( ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) → ( ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) ) |

12 | 11 | com3l | ⊢ ( ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) → ( 𝐺 ∈ GrpOp → ( ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) → 𝐺 ∈ MndOp ) ) ) |

13 | 7 12 | syl | ⊢ ( ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ∧ ∃ 𝑤 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑦 ) = 𝑥 ∧ ( 𝑦 𝐺 𝑤 ) = 𝑥 ) ) → ( 𝐺 ∈ GrpOp → ( ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) → 𝐺 ∈ MndOp ) ) ) |

14 | 4 13 | mpcom | ⊢ ( 𝐺 ∈ GrpOp → ( ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) → 𝐺 ∈ MndOp ) ) |

15 | 14 | expdcom | ⊢ ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) → ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) ) |

16 | 15 | a1i | ⊢ ( ∃ 𝑤 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑤 ) → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) → ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) ) ) |

17 | 16 | com13 | ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) → ( ∃ 𝑤 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑤 ) → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) ) ) |

18 | 17 | 3imp | ⊢ ( ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑤 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑤 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑤 ) ) → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) |

19 | 3 18 | syli | ⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) ) |

20 | 19 | pm2.43i | ⊢ ( 𝐺 ∈ GrpOp → 𝐺 ∈ MndOp ) |