Theorem iscmnd

Description: Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	iscmnd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	iscmnd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
	iscmnd.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	iscmnd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
Assertion	iscmnd	⊢ ( 𝜑 → 𝐺 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		iscmnd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		iscmnd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		iscmnd.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
4		iscmnd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
5	4	3expib	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
6	5	ralrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
7	2	oveqd	⊢ ( 𝜑 → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
8	2	oveqd	⊢ ( 𝜑 → ( 𝑦 + 𝑥 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
9	7 8	eqeq12d	⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
10	1 9	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
11	1 10	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
12	11	anbi2d	⊢ ( 𝜑 → ( ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
13	3 6 12	mpbi2and	⊢ ( 𝜑 → ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
14		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
15		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
16	14 15	iscmn	⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
17	13 16	sylibr	⊢ ( 𝜑 → 𝐺 ∈ CMnd )