This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )