Metamath Proof Explorer


Theorem insubm

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

Ref Expression
Assertion insubm ASubMndMBSubMndMABSubMndM

Proof

Step Hyp Ref Expression
1 submrcl ASubMndMMMnd
2 ssinss1 ABaseMABBaseM
3 2 3ad2ant1 ABaseM0MAaAbAa+MbAABBaseM
4 3 ad2antrl MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBABBaseM
5 elin 0MAB0MA0MB
6 5 simplbi2com 0MB0MA0MAB
7 6 3ad2ant2 BBaseM0MBaBbBa+MbB0MA0MAB
8 7 com12 0MABBaseM0MBaBbBa+MbB0MAB
9 8 3ad2ant2 ABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbB0MAB
10 9 imp ABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbB0MAB
11 10 adantl MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbB0MAB
12 elin xABxAxB
13 elin yAByAyB
14 12 13 anbi12i xAByABxAxByAyB
15 oveq1 a=xa+Mb=x+Mb
16 15 eleq1d a=xa+MbAx+MbA
17 oveq2 b=yx+Mb=x+My
18 17 eleq1d b=yx+MbAx+MyA
19 simpl xAxBxA
20 19 adantr xAxByAyBxA
21 eqidd xAxByAyBa=xA=A
22 simpl yAyByA
23 22 adantl xAxByAyByA
24 16 18 20 21 23 rspc2vd xAxByAyBaAbAa+MbAx+MyA
25 24 com12 aAbAa+MbAxAxByAyBx+MyA
26 25 3ad2ant3 ABaseM0MAaAbAa+MbAxAxByAyBx+MyA
27 26 ad2antrl MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyA
28 27 imp MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyA
29 15 eleq1d a=xa+MbBx+MbB
30 17 eleq1d b=yx+MbBx+MyB
31 simpr xAxBxB
32 31 adantr xAxByAyBxB
33 eqidd xAxByAyBa=xB=B
34 simpr yAyByB
35 34 adantl xAxByAyByB
36 29 30 32 33 35 rspc2vd xAxByAyBaBbBa+MbBx+MyB
37 36 com12 aBbBa+MbBxAxByAyBx+MyB
38 37 3ad2ant3 BBaseM0MBaBbBa+MbBxAxByAyBx+MyB
39 38 adantl ABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyB
40 39 adantl MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyB
41 40 imp MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyB
42 28 41 elind MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyAB
43 42 ex MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAxByAyBx+MyAB
44 14 43 syl5bi MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAByABx+MyAB
45 44 ralrimivv MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBxAByABx+MyAB
46 4 11 45 3jca MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBABBaseM0MABxAByABx+MyAB
47 46 ex MMndABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbBABBaseM0MABxAByABx+MyAB
48 eqid BaseM=BaseM
49 eqid 0M=0M
50 eqid +M=+M
51 48 49 50 issubm MMndASubMndMABaseM0MAaAbAa+MbA
52 48 49 50 issubm MMndBSubMndMBBaseM0MBaBbBa+MbB
53 51 52 anbi12d MMndASubMndMBSubMndMABaseM0MAaAbAa+MbABBaseM0MBaBbBa+MbB
54 48 49 50 issubm MMndABSubMndMABBaseM0MABxAByABx+MyAB
55 47 53 54 3imtr4d MMndASubMndMBSubMndMABSubMndM
56 55 expd MMndASubMndMBSubMndMABSubMndM
57 1 56 mpcom ASubMndMBSubMndMABSubMndM
58 57 imp ASubMndMBSubMndMABSubMndM