This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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 )