Theorem iscsgrpALT

Description: The predicate "is a commutative semigroup". (Contributed by AV, 20-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	ismgmALT.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	ismgmALT.o	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	iscsgrpALT	⊢ ( 𝑀 ∈ CSGrpALT ↔ ( 𝑀 ∈ SGrpALT ∧ ⚬ comLaw 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ismgmALT.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		ismgmALT.o	⊢ ⚬ = ( +g ‘ 𝑀 )
3		fveq2	⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
4		fveq2	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
5	3 4	breq12d	⊢ ( 𝑚 = 𝑀 → ( ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) ↔ ( +g ‘ 𝑀 ) comLaw ( Base ‘ 𝑀 ) ) )
6	2 1	breq12i	⊢ ( ⚬ comLaw 𝐵 ↔ ( +g ‘ 𝑀 ) comLaw ( Base ‘ 𝑀 ) )
7	5 6	bitr4di	⊢ ( 𝑚 = 𝑀 → ( ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) ↔ ⚬ comLaw 𝐵 ) )
8		df-csgrp2	⊢ CSGrpALT = { 𝑚 ∈ SGrpALT ∣ ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) }
9	7 8	elrab2	⊢ ( 𝑀 ∈ CSGrpALT ↔ ( 𝑀 ∈ SGrpALT ∧ ⚬ comLaw 𝐵 ) )