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 syl5bi ( ( 𝑀 ∈ 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 ‘ 𝑀 ) )