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 )