Metamath Proof Explorer

Theorem issgrp

Description: The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 issgrp.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 issgrp.o ⊢ ⚬ = ( +g ‘ 𝑀 )
3 fvexd ⊢ ( 𝑔 = 𝑀 → ( Base ‘ 𝑔 ) ∈ V )
4 fveq2 ⊢ ( 𝑔 = 𝑀 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑀 ) )
5 4 1 eqtr4di ⊢ ( 𝑔 = 𝑀 → ( Base ‘ 𝑔 ) = 𝐵 )
6 fvexd ⊢ ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑔 ) ∈ V )
7 fveq2 ⊢ ( 𝑔 = 𝑀 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝑀 ) )
8 7 adantr ⊢ ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑔 ) = ( +g ‘ 𝑀 ) )
9 8 2 eqtr4di ⊢ ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑔 ) = ⚬ )
10 simplr ⊢ ( ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵 )
11 id ⊢ ( 𝑜 = ⚬ → 𝑜 = ⚬ )
12 oveq ⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
13 eqidd ⊢ ( 𝑜 = ⚬ → 𝑧 = 𝑧 )
14 11 12 13 oveq123d ⊢ ( 𝑜 = ⚬ → ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) )
15 eqidd ⊢ ( 𝑜 = ⚬ → 𝑥 = 𝑥 )
16 oveq ⊢ ( 𝑜 = ⚬ → ( 𝑦 𝑜 𝑧 ) = ( 𝑦 ⚬ 𝑧 ) )
17 11 15 16 oveq123d ⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
18 14 17 eqeq12d ⊢ ( 𝑜 = ⚬ → ( ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
19 18 adantl ⊢ ( ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
20 10 19 raleqbidv ⊢ ( ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
21 10 20 raleqbidv ⊢ ( ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
22 10 21 raleqbidv ⊢ ( ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
23 6 9 22 sbcied2 ⊢ ( ( 𝑔 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
24 3 5 23 sbcied2 ⊢ ( 𝑔 = 𝑀 → ( [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
25 df-sgrp ⊢ Smgrp = { 𝑔 ∈ Mgm ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }
26 24 25 elrab2 ⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )