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

Metamath Proof Explorer

Theorem issgrpv

Description: The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020)

Ref Expression
Hypotheses issgrpn0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
issgrpn0.o ⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion issgrpv ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Smgrp ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 issgrpn0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 issgrpn0.o ⊢ ⚬ = ( +g ‘ 𝑀 )
3 1 2 ismgm ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
4 3 anbi1d ⊢ ( 𝑀 ∈ 𝑉 → ( ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )
5 1 2 issgrp ⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
6 r19.26-2 ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
7 4 5 6 3bitr4g ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Smgrp ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )