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

Metamath Proof Explorer

Theorem issubmndb

Description: The submonoid predicate. Analogous to issubg . (Contributed by AV, 1-Feb-2024)

Ref Expression
Hypotheses issubmndb.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
issubmndb.z ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion issubmndb ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 issubmndb.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 issubmndb.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 eqid ⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
4 1 2 3 issubm2 ⊢ ( 𝐺 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) ) )
5 3anrot ⊢ ( ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) )
6 3anass ⊢ ( ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ↔ ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) )
7 5 6 bitr3i ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) ↔ ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) )
8 4 7 bitrdi ⊢ ( 𝐺 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) ) )
9 8 pm5.32i ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ Mnd ∧ ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) ) )
10 submrcl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
11 10 pm4.71ri ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) )
12 anass ⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) ↔ ( 𝐺 ∈ Mnd ∧ ( ( 𝐺 ↾s 𝑆 ) ∈ Mnd ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) ) )
13 9 11 12 3bitr4i ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) )