Metamath Proof Explorer


Theorem insubm

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

Ref Expression
Assertion insubm A SubMnd M B SubMnd M A B SubMnd M

Proof

Step Hyp Ref Expression
1 submrcl A SubMnd M M Mnd
2 ssinss1 A Base M A B Base M
3 2 3ad2ant1 A Base M 0 M A a A b A a + M b A A B Base M
4 3 ad2antrl M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B A B Base M
5 elin 0 M A B 0 M A 0 M B
6 5 simplbi2com 0 M B 0 M A 0 M A B
7 6 3ad2ant2 B Base M 0 M B a B b B a + M b B 0 M A 0 M A B
8 7 com12 0 M A B Base M 0 M B a B b B a + M b B 0 M A B
9 8 3ad2ant2 A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B 0 M A B
10 9 imp A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B 0 M A B
11 10 adantl M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B 0 M A B
12 elin x A B x A x B
13 elin y A B y A y B
14 12 13 anbi12i x A B y A B x A x B y A y B
15 oveq1 a = x a + M b = x + M b
16 15 eleq1d a = x a + M b A x + M b A
17 oveq2 b = y x + M b = x + M y
18 17 eleq1d b = y x + M b A x + M y A
19 simpl x A x B x A
20 19 adantr x A x B y A y B x A
21 eqidd x A x B y A y B a = x A = A
22 simpl y A y B y A
23 22 adantl x A x B y A y B y A
24 16 18 20 21 23 rspc2vd x A x B y A y B a A b A a + M b A x + M y A
25 24 com12 a A b A a + M b A x A x B y A y B x + M y A
26 25 3ad2ant3 A Base M 0 M A a A b A a + M b A x A x B y A y B x + M y A
27 26 ad2antrl M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y A
28 27 imp M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y A
29 15 eleq1d a = x a + M b B x + M b B
30 17 eleq1d b = y x + M b B x + M y B
31 simpr x A x B x B
32 31 adantr x A x B y A y B x B
33 eqidd x A x B y A y B a = x B = B
34 simpr y A y B y B
35 34 adantl x A x B y A y B y B
36 29 30 32 33 35 rspc2vd x A x B y A y B a B b B a + M b B x + M y B
37 36 com12 a B b B a + M b B x A x B y A y B x + M y B
38 37 3ad2ant3 B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y B
39 38 adantl A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y B
40 39 adantl M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y B
41 40 imp M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y B
42 28 41 elind M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y A B
43 42 ex M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A x B y A y B x + M y A B
44 14 43 syl5bi M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A B y A B x + M y A B
45 44 ralrimivv M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B x A B y A B x + M y A B
46 4 11 45 3jca M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B A B Base M 0 M A B x A B y A B x + M y A B
47 46 ex M Mnd A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B A B Base M 0 M A B x A B y A B x + M y A B
48 eqid Base M = Base M
49 eqid 0 M = 0 M
50 eqid + M = + M
51 48 49 50 issubm M Mnd A SubMnd M A Base M 0 M A a A b A a + M b A
52 48 49 50 issubm M Mnd B SubMnd M B Base M 0 M B a B b B a + M b B
53 51 52 anbi12d M Mnd A SubMnd M B SubMnd M A Base M 0 M A a A b A a + M b A B Base M 0 M B a B b B a + M b B
54 48 49 50 issubm M Mnd A B SubMnd M A B Base M 0 M A B x A B y A B x + M y A B
55 47 53 54 3imtr4d M Mnd A SubMnd M B SubMnd M A B SubMnd M
56 55 expd M Mnd A SubMnd M B SubMnd M A B SubMnd M
57 1 56 mpcom A SubMnd M B SubMnd M A B SubMnd M
58 57 imp A SubMnd M B SubMnd M A B SubMnd M