Metamath Proof Explorer

Theorem insubm

Description: The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024)

Ref Expression
Assertion insubm ( ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 submrcl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )
2 ssinss1 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝑀 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( Base ‘ 𝑀 ) )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( Base ‘ 𝑀 ) )
4 3 ad2antrl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( Base ‘ 𝑀 ) )
5 elin ⊢ ( ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) )
6 5 simplbi2com ⊢ ( ( 0g ‘ 𝑀 ) ∈ 𝐵 → ( ( 0g ‘ 𝑀 ) ∈ 𝐴 → ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
7 6 3ad2ant2 ⊢ ( ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝑀 ) ∈ 𝐴 → ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
8 7 com12 ⊢ ( ( 0g ‘ 𝑀 ) ∈ 𝐴 → ( ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) → ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
9 8 3ad2ant2 ⊢ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) → ( ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) → ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
10 9 imp ⊢ ( ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) )
11 10 adantl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) )
12 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
13 elin ⊢ ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
14 12 13 anbi12i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
15 oveq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑏 ) )
16 15 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ↔ ( 𝑥 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) )
17 oveq2 ⊢ ( 𝑏 = 𝑦 → ( 𝑥 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
18 17 eleq1d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ↔ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐴 ) )
19 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
20 19 adantr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
21 eqidd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 = 𝑥 ) → 𝐴 = 𝐴 )
22 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐴 )
23 22 adantl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐴 )
24 16 18 20 21 23 rspc2vd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐴 ) )
25 24 com12 ⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐴 ) )
26 25 3ad2ant3 ⊢ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐴 ) )
27 26 ad2antrl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐴 ) )
28 27 imp ⊢ ( ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐴 )
29 15 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ↔ ( 𝑥 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) )
30 17 eleq1d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ↔ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) )
31 simpr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
32 31 adantr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
33 eqidd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 = 𝑥 ) → 𝐵 = 𝐵 )
34 simpr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
35 34 adantl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
36 29 30 32 33 35 rspc2vd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) )
37 36 com12 ⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) )
38 37 3ad2ant3 ⊢ ( ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) )
39 38 adantl ⊢ ( ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) )
40 39 adantl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) )
41 40 imp ⊢ ( ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
42 28 41 elind ⊢ ( ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) )
43 42 ex ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
44 14 43 biimtrid ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
45 44 ralrimivv ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) )
46 4 11 45 3jca ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
47 46 ex ⊢ ( 𝑀 ∈ Mnd → ( ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) ) ) )
48 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
49 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
50 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
51 48 49 50 issubm ⊢ ( 𝑀 ∈ Mnd → ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ) )
52 48 49 50 issubm ⊢ ( 𝑀 ∈ Mnd → ( 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) )
53 51 52 anbi12d ⊢ ( 𝑀 ∈ Mnd → ( ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ) ↔ ( ( 𝐴 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐴 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) ) ) )
54 48 49 50 issubm ⊢ ( 𝑀 ∈ Mnd → ( ( 𝐴 ∩ 𝐵 ) ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ ( 𝐴 ∩ 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝐴 ∩ 𝐵 ) ) ) )
55 47 53 54 3imtr4d ⊢ ( 𝑀 ∈ Mnd → ( ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubMnd ‘ 𝑀 ) ) )
56 55 expd ⊢ ( 𝑀 ∈ Mnd → ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝐵 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubMnd ‘ 𝑀 ) ) ) )
57 1 56 mpcom ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝐵 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubMnd ‘ 𝑀 ) ) )
58 57 imp ⊢ ( ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubMnd ‘ 𝑀 ) )