Theorem sgrpplusgaopALT

Description: Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sgrpplusgaopALT	⊢ ( 𝐺 ∈ Smgrp → ( +g ‘ 𝐺 ) assLaw ( Base ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐺 ∈ Mgm ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4	2 3	issgrp	⊢ ( 𝐺 ∈ Smgrp ↔ ( 𝐺 ∈ Mgm ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
5		fvex	⊢ ( +g ‘ 𝐺 ) ∈ V
6		fvex	⊢ ( Base ‘ 𝐺 ) ∈ V
7		isasslaw	⊢ ( ( ( +g ‘ 𝐺 ) ∈ V ∧ ( Base ‘ 𝐺 ) ∈ V ) → ( ( +g ‘ 𝐺 ) assLaw ( Base ‘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
8	5 6 7	mp2an	⊢ ( ( +g ‘ 𝐺 ) assLaw ( Base ‘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
9	1 4 8	3imtr4i	⊢ ( 𝐺 ∈ Smgrp → ( +g ‘ 𝐺 ) assLaw ( Base ‘ 𝐺 ) )