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 )