Theorem iscmn

Description: The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	iscmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscmn.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	iscmn	⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscmn.p	⊢ + = ( +g ‘ 𝐺 )
3		fveq2	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
4	3 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
5		raleq	⊢ ( ( Base ‘ 𝑔 ) = 𝐵 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ) )
6	5	raleqbi1dv	⊢ ( ( Base ‘ 𝑔 ) = 𝐵 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ) )
7	4 6	syl	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ) )
8		fveq2	⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) )
9	8 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = + )
10	9	oveqd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
11	9	oveqd	⊢ ( 𝑔 = 𝐺 → ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) = ( 𝑦 + 𝑥 ) )
12	10 11	eqeq12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ↔ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
13	12	2ralbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
14	7 13	bitrd	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
15		df-cmn	⊢ CMnd = { 𝑔 ∈ Mnd ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑔 ) 𝑥 ) }
16	14 15	elrab2	⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )