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 ⁡ G x G y G z = x G y G z ∧ ∃ w ∈ ran ⁡ G ∀ x ∈ ran ⁡ G w G x = x ∧ ∃ y ∈ ran ⁡ G y G x = w
3 2 biimpd ⊢ G ∈ GrpOp → G ∈ GrpOp → G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ ∃ w ∈ ran ⁡ G ∀ x ∈ ran ⁡ G w G x = x ∧ ∃ y ∈ ran ⁡ G y G x = w
4 1 grpoidinv ⊢ G ∈ GrpOp → ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y ∧ ∃ w ∈ ran ⁡ G w G y = x ∧ y G w = x
5 simpl ⊢ x G y = y ∧ y G x = y ∧ ∃ w ∈ ran ⁡ G w G y = x ∧ y G w = x → x G y = y ∧ y G x = y
6 5 ralimi ⊢ ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y ∧ ∃ w ∈ ran ⁡ G w G y = x ∧ y G w = x → ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y
7 6 reximi ⊢ ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y ∧ ∃ w ∈ ran ⁡ G w G y = x ∧ y G w = x → ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y
8 1 ismndo2 ⊢ G ∈ GrpOp → G ∈ MndOp ↔ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y
9 8 biimprcd ⊢ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y → G ∈ GrpOp → G ∈ MndOp
10 9 3exp ⊢ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z → ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y → G ∈ GrpOp → G ∈ MndOp
11 10 impcom ⊢ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G → ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y → G ∈ GrpOp → G ∈ MndOp
12 11 com3l ⊢ ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G → G ∈ MndOp
13 7 12 syl ⊢ ∃ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y ∧ y G x = y ∧ ∃ w ∈ ran ⁡ G w G y = x ∧ y G w = x → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G → G ∈ MndOp
14 4 13 mpcom ⊢ G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G → G ∈ MndOp
15 14 expdcom ⊢ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z → G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G → G ∈ GrpOp → G ∈ MndOp
16 15 a1i ⊢ ∃ w ∈ ran ⁡ G ∀ x ∈ ran ⁡ G w G x = x ∧ ∃ y ∈ ran ⁡ G y G x = w → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z → 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 ⁡ G x G y G z = x G y G z → ∃ w ∈ ran ⁡ G ∀ x ∈ ran ⁡ G w G x = x ∧ ∃ y ∈ ran ⁡ G y G x = w → G ∈ GrpOp → G ∈ MndOp
18 17 3imp ⊢ G : ran ⁡ G × ran ⁡ G ⟶ ran ⁡ G ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G ∀ z ∈ ran ⁡ G x G y G z = x G y G z ∧ ∃ w ∈ ran ⁡ G ∀ x ∈ ran ⁡ G w G x = x ∧ ∃ y ∈ ran ⁡ G y G x = w → G ∈ GrpOp → G ∈ MndOp
19 3 18 syli ⊢ G ∈ GrpOp → G ∈ GrpOp → G ∈ MndOp
20 19 pm2.43i ⊢ G ∈ GrpOp → G ∈ MndOp