Metamath Proof Explorer

Theorem ismnddef

Description: The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009) (Revised by AV, 1-Feb-2020)

Ref Expression
Hypotheses ismnddef.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ismnddef.p ⊢ + = ( +g ‘ 𝐺 )
Assertion ismnddef ( 𝐺 ∈ Mnd ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )

Proof

Step Hyp Ref Expression
1 ismnddef.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ismnddef.p ⊢ + = ( +g ‘ 𝐺 )
3 fvex ⊢ ( Base ‘ 𝑔 ) ∈ V
4 fvex ⊢ ( +g ‘ 𝑔 ) ∈ V
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
7 6 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 = ( Base ‘ 𝑔 ) ↔ 𝑏 = 𝐵 ) )
8 fveq2 ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) )
9 8 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = + )
10 9 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑝 = ( +g ‘ 𝑔 ) ↔ 𝑝 = + ) )
11 7 10 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑏 = ( Base ‘ 𝑔 ) ∧ 𝑝 = ( +g ‘ 𝑔 ) ) ↔ ( 𝑏 = 𝐵 ∧ 𝑝 = + ) ) )
12 simpl ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑝 = + ) → 𝑏 = 𝐵 )
13 oveq ⊢ ( 𝑝 = + → ( 𝑒 𝑝 𝑎 ) = ( 𝑒 + 𝑎 ) )
14 13 eqeq1d ⊢ ( 𝑝 = + → ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ↔ ( 𝑒 + 𝑎 ) = 𝑎 ) )
15 oveq ⊢ ( 𝑝 = + → ( 𝑎 𝑝 𝑒 ) = ( 𝑎 + 𝑒 ) )
16 15 eqeq1d ⊢ ( 𝑝 = + → ( ( 𝑎 𝑝 𝑒 ) = 𝑎 ↔ ( 𝑎 + 𝑒 ) = 𝑎 ) )
17 14 16 anbi12d ⊢ ( 𝑝 = + → ( ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) ↔ ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
18 17 adantl ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑝 = + ) → ( ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) ↔ ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
19 12 18 raleqbidv ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑝 = + ) → ( ∀ 𝑎 ∈ 𝑏 ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
20 12 19 rexeqbidv ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑝 = + ) → ( ∃ 𝑒 ∈ 𝑏 ∀ 𝑎 ∈ 𝑏 ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) ↔ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
21 11 20 syl6bi ⊢ ( 𝑔 = 𝐺 → ( ( 𝑏 = ( Base ‘ 𝑔 ) ∧ 𝑝 = ( +g ‘ 𝑔 ) ) → ( ∃ 𝑒 ∈ 𝑏 ∀ 𝑎 ∈ 𝑏 ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) ↔ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) ) )
22 3 4 21 sbc2iedv ⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑎 ∈ 𝑏 ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) ↔ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
23 df-mnd ⊢ Mnd = { 𝑔 ∈ Smgrp ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑎 ∈ 𝑏 ( ( 𝑒 𝑝 𝑎 ) = 𝑎 ∧ ( 𝑎 𝑝 𝑒 ) = 𝑎 ) }
24 22 23 elrab2 ⊢ ( 𝐺 ∈ Mnd ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )