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

Metamath Proof Explorer

Theorem rabsubmgmd

Description: Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypotheses rabsubmgmd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
rabsubmgmd.p ⊢ + = ( +g ‘ 𝑀 )
rabsubmgmd.m ⊢ ( 𝜑 → 𝑀 ∈ Mgm )
rabsubmgmd.cp ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ) → 𝜂 )
rabsubmgmd.th ⊢ ( 𝑧 = 𝑥 → ( 𝜓 ↔ 𝜃 ) )
rabsubmgmd.ta ⊢ ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜏 ) )
rabsubmgmd.et ⊢ ( 𝑧 = ( 𝑥 + 𝑦 ) → ( 𝜓 ↔ 𝜂 ) )
Assertion rabsubmgmd ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMgm ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 rabsubmgmd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 rabsubmgmd.p ⊢ + = ( +g ‘ 𝑀 )
3 rabsubmgmd.m ⊢ ( 𝜑 → 𝑀 ∈ Mgm )
4 rabsubmgmd.cp ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ) → 𝜂 )
5 rabsubmgmd.th ⊢ ( 𝑧 = 𝑥 → ( 𝜓 ↔ 𝜃 ) )
6 rabsubmgmd.ta ⊢ ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜏 ) )
7 rabsubmgmd.et ⊢ ( 𝑧 = ( 𝑥 + 𝑦 ) → ( 𝜓 ↔ 𝜂 ) )
8 ssrab2 ⊢ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵
9 8 a1i ⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵 )
10 5 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) )
11 6 elrab ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) )
12 10 11 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝑀 ∈ Mgm )
14 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝑥 ∈ 𝐵 )
15 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝑦 ∈ 𝐵 )
16 1 2 mgmcl ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
17 13 14 15 16 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
18 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) → 𝑥 ∈ 𝐵 )
19 simpl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) → 𝑦 ∈ 𝐵 )
20 18 19 anim12i ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
21 simpr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) → 𝜃 )
22 simpr ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) → 𝜏 )
23 21 22 anim12i ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) → ( 𝜃 ∧ 𝜏 ) )
24 20 23 jca ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝜃 ∧ 𝜏 ) ) )
25 24 4 sylan2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → 𝜂 )
26 7 17 25 elrabd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝜃 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜏 ) ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
27 12 26 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
28 27 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } )
29 1 2 issubmgm ⊢ ( 𝑀 ∈ Mgm → ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMgm ‘ 𝑀 ) ↔ ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ) )
30 3 29 syl ⊢ ( 𝜑 → ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMgm ‘ 𝑀 ) ↔ ( { 𝑧 ∈ 𝐵 ∣ 𝜓 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ( 𝑥 + 𝑦 ) ∈ { 𝑧 ∈ 𝐵 ∣ 𝜓 } ) ) )
31 9 28 30 mpbir2and ⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝜓 } ∈ ( SubMgm ‘ 𝑀 ) )