Metamath Proof Explorer

Theorem issubmndb

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

Ref Expression
Hypotheses issubmndb.b ⊢ B = Base G
issubmndb.z ⊢ 0 ˙ = 0 G
Assertion issubmndb ⊢ S ∈ SubMnd ⁡ G ↔ G ∈ Mnd ∧ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S

Proof

Step Hyp Ref Expression
1 issubmndb.b ⊢ B = Base G
2 issubmndb.z ⊢ 0 ˙ = 0 G
3 eqid ⊢ G ↾ 𝑠 S = G ↾ 𝑠 S
4 1 2 3 issubm2 ⊢ G ∈ Mnd → S ∈ SubMnd ⁡ G ↔ S ⊆ B ∧ 0 ˙ ∈ S ∧ G ↾ 𝑠 S ∈ Mnd
5 3anrot ⊢ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ↔ S ⊆ B ∧ 0 ˙ ∈ S ∧ G ↾ 𝑠 S ∈ Mnd
6 3anass ⊢ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ↔ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S
7 5 6 bitr3i ⊢ S ⊆ B ∧ 0 ˙ ∈ S ∧ G ↾ 𝑠 S ∈ Mnd ↔ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S
8 4 7 bitrdi ⊢ G ∈ Mnd → S ∈ SubMnd ⁡ G ↔ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S
9 8 pm5.32i ⊢ G ∈ Mnd ∧ S ∈ SubMnd ⁡ G ↔ G ∈ Mnd ∧ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S
10 submrcl ⊢ S ∈ SubMnd ⁡ G → G ∈ Mnd
11 10 pm4.71ri ⊢ S ∈ SubMnd ⁡ G ↔ G ∈ Mnd ∧ S ∈ SubMnd ⁡ G
12 anass ⊢ G ∈ Mnd ∧ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ↔ G ∈ Mnd ∧ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S
13 9 11 12 3bitr4i ⊢ S ∈ SubMnd ⁡ G ↔ G ∈ Mnd ∧ G ↾ 𝑠 S ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S