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 ∈ 𝑆 ) ) )