Metamath Proof Explorer

Theorem issubmd

Description: Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses issubmd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
issubmd.p ⊢ + = ( +g ‘ 𝑀 )
issubmd.z ⊢ 0 = ( 0g ‘ 𝑀 )
issubmd.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
issubmd.cz ⊢ ( 𝜑 → 𝜒 )
issubmd.cp ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ) → 𝜂 )
issubmd.ch ⊢ ( 𝑧 = 0 → ( 𝜓 ↔ 𝜒 ) )
issubmd.th ⊢ ( 𝑧 = 𝑥 → ( 𝜓 ↔ 𝜃 ) )
issubmd.ta ⊢ ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜏 ) )
issubmd.et ⊢ ( 𝑧 = ( 𝑥 + 𝑦 ) → ( 𝜓 ↔ 𝜂 ) )
Assertion issubmd ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 issubmd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 issubmd.p ⊢ + = ( +g ‘ 𝑀 )
3 issubmd.z ⊢ 0 = ( 0g ‘ 𝑀 )
4 issubmd.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
5 issubmd.cz ⊢ ( 𝜑 → 𝜒 )
6 issubmd.cp ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ) → 𝜂 )
7 issubmd.ch ⊢ ( 𝑧 = 0 → ( 𝜓 ↔ 𝜒 ) )
8 issubmd.th ⊢ ( 𝑧 = 𝑥 → ( 𝜓 ↔ 𝜃 ) )
9 issubmd.ta ⊢ ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜏 ) )
10 issubmd.et ⊢ ( 𝑧 = ( 𝑥 + 𝑦 ) → ( 𝜓 ↔ 𝜂 ) )
11 ssrab2 ⊢ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵
12 11 a1i ⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵 )
13 1 3 mndidcl ⊢ ( 𝑀 ∈ Mnd → 0 ∈ 𝐵 )
14 4 13 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
15 7 14 5 elrabd ⊢ ( 𝜑 → 0 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
16 8 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) )
17 9 elrab ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) )
18 16 17 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) )
19 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝑀 ∈ Mnd )
20 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝑥 ∈ 𝐵 )
21 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝑦 ∈ 𝐵 )
22 1 2 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
23 19 20 21 22 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
24 an4 ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝜃 ∧ 𝜏 ) ) )
25 24 6 sylan2b ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝜂 )
26 10 23 25 elrabd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
27 18 26 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
28 27 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
29 1 3 2 issubm ⊢ ( 𝑀 ∈ Mnd → ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMnd ‘ 𝑀 ) ↔ ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵 ∧ 0 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∧ ∀ 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ) )
30 4 29 syl ⊢ ( 𝜑 → ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMnd ‘ 𝑀 ) ↔ ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵 ∧ 0 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∧ ∀ 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ) )
31 12 15 28 30 mpbir3and ⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMnd ‘ 𝑀 ) )