Step | Hyp | Ref
| Expression |
1 | | submrcl 18618 |
. . . 4
β’ (π β (SubMndβπΊ) β πΊ β Mnd) |
2 | 1 | 3ad2ant1 1134 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β πΊ β Mnd) |
3 | | eqid 2733 |
. . . . 5
β’
(BaseβπΊ) =
(BaseβπΊ) |
4 | 3 | submss 18625 |
. . . 4
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
5 | 4 | 3ad2ant1 1134 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β π β (BaseβπΊ)) |
6 | 3 | submss 18625 |
. . . 4
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
7 | 6 | 3ad2ant2 1135 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β π β (BaseβπΊ)) |
8 | | lsmsubg.p |
. . . 4
β’ β =
(LSSumβπΊ) |
9 | 3, 8 | lsmssv 19430 |
. . 3
β’ ((πΊ β Mnd β§ π β (BaseβπΊ) β§ π β (BaseβπΊ)) β (π β π) β (BaseβπΊ)) |
10 | 2, 5, 7, 9 | syl3anc 1372 |
. 2
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (π β π) β (BaseβπΊ)) |
11 | | simp2 1138 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β π β (SubMndβπΊ)) |
12 | 3, 8 | lsmub1x 19433 |
. . . 4
β’ ((π β (BaseβπΊ) β§ π β (SubMndβπΊ)) β π β (π β π)) |
13 | 5, 11, 12 | syl2anc 585 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β π β (π β π)) |
14 | | eqid 2733 |
. . . . 5
β’
(0gβπΊ) = (0gβπΊ) |
15 | 14 | subm0cl 18627 |
. . . 4
β’ (π β (SubMndβπΊ) β
(0gβπΊ)
β π) |
16 | 15 | 3ad2ant1 1134 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (0gβπΊ) β π) |
17 | 13, 16 | sseldd 3946 |
. 2
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (0gβπΊ) β (π β π)) |
18 | | eqid 2733 |
. . . . . . 7
β’
(+gβπΊ) = (+gβπΊ) |
19 | 3, 18, 8 | lsmelvalx 19427 |
. . . . . 6
β’ ((πΊ β Mnd β§ π β (BaseβπΊ) β§ π β (BaseβπΊ)) β (π₯ β (π β π) β βπ β π βπ β π π₯ = (π(+gβπΊ)π))) |
20 | 2, 5, 7, 19 | syl3anc 1372 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (π₯ β (π β π) β βπ β π βπ β π π₯ = (π(+gβπΊ)π))) |
21 | 3, 18, 8 | lsmelvalx 19427 |
. . . . . 6
β’ ((πΊ β Mnd β§ π β (BaseβπΊ) β§ π β (BaseβπΊ)) β (π¦ β (π β π) β βπ β π βπ β π π¦ = (π(+gβπΊ)π))) |
22 | 2, 5, 7, 21 | syl3anc 1372 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (π¦ β (π β π) β βπ β π βπ β π π¦ = (π(+gβπΊ)π))) |
23 | 20, 22 | anbi12d 632 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β ((π₯ β (π β π) β§ π¦ β (π β π)) β (βπ β π βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π βπ β π π¦ = (π(+gβπΊ)π)))) |
24 | | reeanv 3216 |
. . . . 5
β’
(βπ β
π βπ β π (βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π π¦ = (π(+gβπΊ)π)) β (βπ β π βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π βπ β π π¦ = (π(+gβπΊ)π))) |
25 | | reeanv 3216 |
. . . . . . 7
β’
(βπ β
π βπ β π (π₯ = (π(+gβπΊ)π) β§ π¦ = (π(+gβπΊ)π)) β (βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π π¦ = (π(+gβπΊ)π))) |
26 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β πΊ β Mnd) |
27 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (BaseβπΊ)) |
28 | | simprll 778 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β π) |
29 | 27, 28 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (BaseβπΊ)) |
30 | | simprlr 779 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β π) |
31 | 27, 30 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (BaseβπΊ)) |
32 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (BaseβπΊ)) |
33 | | simprrl 780 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β π) |
34 | 32, 33 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (BaseβπΊ)) |
35 | | simprrr 781 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β π) |
36 | 32, 35 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (BaseβπΊ)) |
37 | | simpl3 1194 |
. . . . . . . . . . . . . 14
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (πβπ)) |
38 | 37, 30 | sseldd 3946 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (πβπ)) |
39 | | lsmsubg.z |
. . . . . . . . . . . . . 14
β’ π = (CntzβπΊ) |
40 | 18, 39 | cntzi 19114 |
. . . . . . . . . . . . 13
β’ ((π β (πβπ) β§ π β π) β (π(+gβπΊ)π) = (π(+gβπΊ)π)) |
41 | 38, 33, 40 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β (π(+gβπΊ)π) = (π(+gβπΊ)π)) |
42 | 3, 18, 26, 29, 31, 34, 36, 41 | mnd4g 18575 |
. . . . . . . . . . 11
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π)) = ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π))) |
43 | | simpl1 1192 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (SubMndβπΊ)) |
44 | 18 | submcl 18628 |
. . . . . . . . . . . . 13
β’ ((π β (SubMndβπΊ) β§ π β π β§ π β π) β (π(+gβπΊ)π) β π) |
45 | 43, 28, 30, 44 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β (π(+gβπΊ)π) β π) |
46 | | simpl2 1193 |
. . . . . . . . . . . . 13
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β π β (SubMndβπΊ)) |
47 | 18 | submcl 18628 |
. . . . . . . . . . . . 13
β’ ((π β (SubMndβπΊ) β§ π β π β§ π β π) β (π(+gβπΊ)π) β π) |
48 | 46, 33, 35, 47 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β (π(+gβπΊ)π) β π) |
49 | 3, 18, 8 | lsmelvalix 19428 |
. . . . . . . . . . . 12
β’ (((πΊ β Mnd β§ π β (BaseβπΊ) β§ π β (BaseβπΊ)) β§ ((π(+gβπΊ)π) β π β§ (π(+gβπΊ)π) β π)) β ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π)) β (π β π)) |
50 | 26, 27, 32, 45, 48, 49 | syl32anc 1379 |
. . . . . . . . . . 11
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π)) β (π β π)) |
51 | 42, 50 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π)) β (π β π)) |
52 | | oveq12 7367 |
. . . . . . . . . . 11
β’ ((π₯ = (π(+gβπΊ)π) β§ π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) = ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π))) |
53 | 52 | eleq1d 2819 |
. . . . . . . . . 10
β’ ((π₯ = (π(+gβπΊ)π) β§ π¦ = (π(+gβπΊ)π)) β ((π₯(+gβπΊ)π¦) β (π β π) β ((π(+gβπΊ)π)(+gβπΊ)(π(+gβπΊ)π)) β (π β π))) |
54 | 51, 53 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ ((π β π β§ π β π) β§ (π β π β§ π β π))) β ((π₯ = (π(+gβπΊ)π) β§ π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
55 | 54 | anassrs 469 |
. . . . . . . 8
β’ ((((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β ((π₯ = (π(+gβπΊ)π) β§ π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
56 | 55 | rexlimdvva 3202 |
. . . . . . 7
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ (π β π β§ π β π)) β (βπ β π βπ β π (π₯ = (π(+gβπΊ)π) β§ π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
57 | 25, 56 | biimtrrid 242 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β§ (π β π β§ π β π)) β ((βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
58 | 57 | rexlimdvva 3202 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (βπ β π βπ β π (βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
59 | 24, 58 | biimtrrid 242 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β ((βπ β π βπ β π π₯ = (π(+gβπΊ)π) β§ βπ β π βπ β π π¦ = (π(+gβπΊ)π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
60 | 23, 59 | sylbid 239 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β ((π₯ β (π β π) β§ π¦ β (π β π)) β (π₯(+gβπΊ)π¦) β (π β π))) |
61 | 60 | ralrimivv 3192 |
. 2
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β βπ₯ β (π β π)βπ¦ β (π β π)(π₯(+gβπΊ)π¦) β (π β π)) |
62 | 3, 14, 18 | issubm 18619 |
. . 3
β’ (πΊ β Mnd β ((π β π) β (SubMndβπΊ) β ((π β π) β (BaseβπΊ) β§ (0gβπΊ) β (π β π) β§ βπ₯ β (π β π)βπ¦ β (π β π)(π₯(+gβπΊ)π¦) β (π β π)))) |
63 | 2, 62 | syl 17 |
. 2
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β ((π β π) β (SubMndβπΊ) β ((π β π) β (BaseβπΊ) β§ (0gβπΊ) β (π β π) β§ βπ₯ β (π β π)βπ¦ β (π β π)(π₯(+gβπΊ)π¦) β (π β π)))) |
64 | 10, 17, 61, 63 | mpbir3and 1343 |
1
β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (π β π) β (SubMndβπΊ)) |