Step | Hyp | Ref
| Expression |
1 | | submrcl 18618 |
. . 3
β’ (π΄ β (SubMndβπ) β π β Mnd) |
2 | | ssinss1 4198 |
. . . . . . . . 9
β’ (π΄ β (Baseβπ) β (π΄ β© π΅) β (Baseβπ)) |
3 | 2 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β (π΄ β© π΅) β (Baseβπ)) |
4 | 3 | ad2antrl 727 |
. . . . . . 7
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β (π΄ β© π΅) β (Baseβπ)) |
5 | | elin 3927 |
. . . . . . . . . . . . 13
β’
((0gβπ) β (π΄ β© π΅) β ((0gβπ) β π΄ β§ (0gβπ) β π΅)) |
6 | 5 | simplbi2com 504 |
. . . . . . . . . . . 12
β’
((0gβπ) β π΅ β ((0gβπ) β π΄ β (0gβπ) β (π΄ β© π΅))) |
7 | 6 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π΅ β (Baseβπ) β§
(0gβπ)
β π΅ β§
βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅) β ((0gβπ) β π΄ β (0gβπ) β (π΄ β© π΅))) |
8 | 7 | com12 32 |
. . . . . . . . . 10
β’
((0gβπ) β π΄ β ((π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅) β (0gβπ) β (π΄ β© π΅))) |
9 | 8 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β ((π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅) β (0gβπ) β (π΄ β© π΅))) |
10 | 9 | imp 408 |
. . . . . . . 8
β’ (((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅)) β (0gβπ) β (π΄ β© π΅)) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β (0gβπ) β (π΄ β© π΅)) |
12 | | elin 3927 |
. . . . . . . . . 10
β’ (π₯ β (π΄ β© π΅) β (π₯ β π΄ β§ π₯ β π΅)) |
13 | | elin 3927 |
. . . . . . . . . 10
β’ (π¦ β (π΄ β© π΅) β (π¦ β π΄ β§ π¦ β π΅)) |
14 | 12, 13 | anbi12i 628 |
. . . . . . . . 9
β’ ((π₯ β (π΄ β© π΅) β§ π¦ β (π΄ β© π΅)) β ((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅))) |
15 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β (π(+gβπ)π) = (π₯(+gβπ)π)) |
16 | 15 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π = π₯ β ((π(+gβπ)π) β π΄ β (π₯(+gβπ)π) β π΄)) |
17 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β (π₯(+gβπ)π) = (π₯(+gβπ)π¦)) |
18 | 17 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π = π¦ β ((π₯(+gβπ)π) β π΄ β (π₯(+gβπ)π¦) β π΄)) |
19 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π΄ β§ π₯ β π΅) β π₯ β π΄) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β π₯ β π΄) |
21 | | eqidd 2734 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β§ π = π₯) β π΄ = π΄) |
22 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β π΄ β§ π¦ β π΅) β π¦ β π΄) |
23 | 22 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β π¦ β π΄) |
24 | 16, 18, 20, 21, 23 | rspc2vd 3907 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄ β (π₯(+gβπ)π¦) β π΄)) |
25 | 24 | com12 32 |
. . . . . . . . . . . . . 14
β’
(βπ β
π΄ βπ β π΄ (π(+gβπ)π) β π΄ β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΄)) |
26 | 25 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΄)) |
27 | 26 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΄)) |
28 | 27 | imp 408 |
. . . . . . . . . . 11
β’ (((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β§ ((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅))) β (π₯(+gβπ)π¦) β π΄) |
29 | 15 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β ((π(+gβπ)π) β π΅ β (π₯(+gβπ)π) β π΅)) |
30 | 17 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β ((π₯(+gβπ)π) β π΅ β (π₯(+gβπ)π¦) β π΅)) |
31 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β π΄ β§ π₯ β π΅) β π₯ β π΅) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β π₯ β π΅) |
33 | | eqidd 2734 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β§ π = π₯) β π΅ = π΅) |
34 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β π΄ β§ π¦ β π΅) β π¦ β π΅) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β π¦ β π΅) |
36 | 29, 30, 32, 33, 35 | rspc2vd 3907 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅ β (π₯(+gβπ)π¦) β π΅)) |
37 | 36 | com12 32 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π΅ βπ β π΅ (π(+gβπ)π) β π΅ β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΅)) |
38 | 37 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π΅ β (Baseβπ) β§
(0gβπ)
β π΅ β§
βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅) β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΅)) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅)) β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΅)) |
40 | 39 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΅)) |
41 | 40 | imp 408 |
. . . . . . . . . . 11
β’ (((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β§ ((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅))) β (π₯(+gβπ)π¦) β π΅) |
42 | 28, 41 | elind 4155 |
. . . . . . . . . 10
β’ (((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β§ ((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅))) β (π₯(+gβπ)π¦) β (π΄ β© π΅)) |
43 | 42 | ex 414 |
. . . . . . . . 9
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β (((π₯ β π΄ β§ π₯ β π΅) β§ (π¦ β π΄ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β (π΄ β© π΅))) |
44 | 14, 43 | biimtrid 241 |
. . . . . . . 8
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β ((π₯ β (π΄ β© π΅) β§ π¦ β (π΄ β© π΅)) β (π₯(+gβπ)π¦) β (π΄ β© π΅))) |
45 | 44 | ralrimivv 3192 |
. . . . . . 7
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β βπ₯ β (π΄ β© π΅)βπ¦ β (π΄ β© π΅)(π₯(+gβπ)π¦) β (π΄ β© π΅)) |
46 | 4, 11, 45 | 3jca 1129 |
. . . . . 6
β’ ((π β Mnd β§ ((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) β ((π΄ β© π΅) β (Baseβπ) β§ (0gβπ) β (π΄ β© π΅) β§ βπ₯ β (π΄ β© π΅)βπ¦ β (π΄ β© π΅)(π₯(+gβπ)π¦) β (π΄ β© π΅))) |
47 | 46 | ex 414 |
. . . . 5
β’ (π β Mnd β (((π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§
βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅)) β ((π΄ β© π΅) β (Baseβπ) β§ (0gβπ) β (π΄ β© π΅) β§ βπ₯ β (π΄ β© π΅)βπ¦ β (π΄ β© π΅)(π₯(+gβπ)π¦) β (π΄ β© π΅)))) |
48 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
49 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
50 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
51 | 48, 49, 50 | issubm 18619 |
. . . . . 6
β’ (π β Mnd β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄))) |
52 | 48, 49, 50 | issubm 18619 |
. . . . . 6
β’ (π β Mnd β (π΅ β (SubMndβπ) β (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅))) |
53 | 51, 52 | anbi12d 632 |
. . . . 5
β’ (π β Mnd β ((π΄ β (SubMndβπ) β§ π΅ β (SubMndβπ)) β ((π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ βπ β π΄ βπ β π΄ (π(+gβπ)π) β π΄) β§ (π΅ β (Baseβπ) β§ (0gβπ) β π΅ β§ βπ β π΅ βπ β π΅ (π(+gβπ)π) β π΅)))) |
54 | 48, 49, 50 | issubm 18619 |
. . . . 5
β’ (π β Mnd β ((π΄ β© π΅) β (SubMndβπ) β ((π΄ β© π΅) β (Baseβπ) β§ (0gβπ) β (π΄ β© π΅) β§ βπ₯ β (π΄ β© π΅)βπ¦ β (π΄ β© π΅)(π₯(+gβπ)π¦) β (π΄ β© π΅)))) |
55 | 47, 53, 54 | 3imtr4d 294 |
. . . 4
β’ (π β Mnd β ((π΄ β (SubMndβπ) β§ π΅ β (SubMndβπ)) β (π΄ β© π΅) β (SubMndβπ))) |
56 | 55 | expd 417 |
. . 3
β’ (π β Mnd β (π΄ β (SubMndβπ) β (π΅ β (SubMndβπ) β (π΄ β© π΅) β (SubMndβπ)))) |
57 | 1, 56 | mpcom 38 |
. 2
β’ (π΄ β (SubMndβπ) β (π΅ β (SubMndβπ) β (π΄ β© π΅) β (SubMndβπ))) |
58 | 57 | imp 408 |
1
β’ ((π΄ β (SubMndβπ) β§ π΅ β (SubMndβπ)) β (π΄ β© π΅) β (SubMndβπ)) |