Step | Hyp | Ref
| Expression |
1 | | cycsubm.c |
. . 3
β’ πΆ = ran πΉ |
2 | | cycsubm.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
3 | | cycsubm.t |
. . . . . . . 8
β’ Β· =
(.gβπΊ) |
4 | 2, 3 | mulgnn0cl 18893 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π₯ β β0
β§ π΄ β π΅) β (π₯ Β· π΄) β π΅) |
5 | 4 | 3expa 1119 |
. . . . . 6
β’ (((πΊ β Mnd β§ π₯ β β0)
β§ π΄ β π΅) β (π₯ Β· π΄) β π΅) |
6 | 5 | an32s 651 |
. . . . 5
β’ (((πΊ β Mnd β§ π΄ β π΅) β§ π₯ β β0) β (π₯ Β· π΄) β π΅) |
7 | | cycsubm.f |
. . . . 5
β’ πΉ = (π₯ β β0 β¦ (π₯ Β· π΄)) |
8 | 6, 7 | fmptd 7063 |
. . . 4
β’ ((πΊ β Mnd β§ π΄ β π΅) β πΉ:β0βΆπ΅) |
9 | 8 | frnd 6677 |
. . 3
β’ ((πΊ β Mnd β§ π΄ β π΅) β ran πΉ β π΅) |
10 | 1, 9 | eqsstrid 3993 |
. 2
β’ ((πΊ β Mnd β§ π΄ β π΅) β πΆ β π΅) |
11 | | 0nn0 12429 |
. . . . 5
β’ 0 β
β0 |
12 | 11 | a1i 11 |
. . . 4
β’ ((πΊ β Mnd β§ π΄ β π΅) β 0 β
β0) |
13 | | oveq1 7365 |
. . . . . 6
β’ (π = 0 β (π Β· π΄) = (0 Β· π΄)) |
14 | 13 | eqeq2d 2748 |
. . . . 5
β’ (π = 0 β
((0gβπΊ) =
(π Β· π΄) β (0gβπΊ) = (0 Β· π΄))) |
15 | 14 | adantl 483 |
. . . 4
β’ (((πΊ β Mnd β§ π΄ β π΅) β§ π = 0) β ((0gβπΊ) = (π Β· π΄) β (0gβπΊ) = (0 Β· π΄))) |
16 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
17 | 2, 16, 3 | mulg0 18880 |
. . . . . 6
β’ (π΄ β π΅ β (0 Β· π΄) = (0gβπΊ)) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((πΊ β Mnd β§ π΄ β π΅) β (0 Β· π΄) = (0gβπΊ)) |
19 | 18 | eqcomd 2743 |
. . . 4
β’ ((πΊ β Mnd β§ π΄ β π΅) β (0gβπΊ) = (0 Β· π΄)) |
20 | 12, 15, 19 | rspcedvd 3584 |
. . 3
β’ ((πΊ β Mnd β§ π΄ β π΅) β βπ β β0
(0gβπΊ) =
(π Β· π΄)) |
21 | 2, 3, 7, 1 | cycsubmel 18994 |
. . 3
β’
((0gβπΊ) β πΆ β βπ β β0
(0gβπΊ) =
(π Β· π΄)) |
22 | 20, 21 | sylibr 233 |
. 2
β’ ((πΊ β Mnd β§ π΄ β π΅) β (0gβπΊ) β πΆ) |
23 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β π β
β0) |
24 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β π β
β0) |
25 | 23, 24 | nn0addcld 12478 |
. . . . . . . . . . 11
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β (π + π) β
β0) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’
(((((πΊ β Mnd
β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β§ (π = (π Β· π΄) β§ π = (π Β· π΄))) β (π + π) β
β0) |
27 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π = (π + π) β (π Β· π΄) = ((π + π) Β· π΄)) |
28 | 27 | eqeq2d 2748 |
. . . . . . . . . . 11
β’ (π = (π + π) β ((π(+gβπΊ)π) = (π Β· π΄) β (π(+gβπΊ)π) = ((π + π) Β· π΄))) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
β’
((((((πΊ β Mnd
β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β§ (π = (π Β· π΄) β§ π = (π Β· π΄))) β§ π = (π + π)) β ((π(+gβπΊ)π) = (π Β· π΄) β (π(+gβπΊ)π) = ((π + π) Β· π΄))) |
30 | | oveq12 7367 |
. . . . . . . . . . . 12
β’ ((π = (π Β· π΄) β§ π = (π Β· π΄)) β (π(+gβπΊ)π) = ((π Β· π΄)(+gβπΊ)(π Β· π΄))) |
31 | 30 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π = (π Β· π΄) β§ π = (π Β· π΄)) β (π(+gβπΊ)π) = ((π Β· π΄)(+gβπΊ)(π Β· π΄))) |
32 | | simplll 774 |
. . . . . . . . . . . . 13
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β πΊ β
Mnd) |
33 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β π΄ β π΅) |
34 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(+gβπΊ) = (+gβπΊ) |
35 | 2, 3, 34 | mulgnn0dir 18907 |
. . . . . . . . . . . . 13
β’ ((πΊ β Mnd β§ (π β β0
β§ π β
β0 β§ π΄
β π΅)) β ((π + π) Β· π΄) = ((π Β· π΄)(+gβπΊ)(π Β· π΄))) |
36 | 32, 23, 24, 33, 35 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β ((π + π) Β· π΄) = ((π Β· π΄)(+gβπΊ)(π Β· π΄))) |
37 | 36 | eqcomd 2743 |
. . . . . . . . . . 11
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β ((π Β· π΄)(+gβπΊ)(π Β· π΄)) = ((π + π) Β· π΄)) |
38 | 31, 37 | sylan9eqr 2799 |
. . . . . . . . . 10
β’
(((((πΊ β Mnd
β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β§ (π = (π Β· π΄) β§ π = (π Β· π΄))) β (π(+gβπΊ)π) = ((π + π) Β· π΄)) |
39 | 26, 29, 38 | rspcedvd 3584 |
. . . . . . . . 9
β’
(((((πΊ β Mnd
β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β§ (π = (π Β· π΄) β§ π = (π Β· π΄))) β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄)) |
40 | 39 | exp32 422 |
. . . . . . . 8
β’ ((((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β§ π β β0)
β (π = (π Β· π΄) β (π = (π Β· π΄) β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄)))) |
41 | 40 | rexlimdva 3153 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β
(βπ β
β0 π =
(π Β· π΄) β (π = (π Β· π΄) β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄)))) |
42 | 41 | com23 86 |
. . . . . 6
β’ (((πΊ β Mnd β§ π΄ β π΅) β§ π β β0) β (π = (π Β· π΄) β (βπ β β0 π = (π Β· π΄) β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄)))) |
43 | 42 | rexlimdva 3153 |
. . . . 5
β’ ((πΊ β Mnd β§ π΄ β π΅) β (βπ β β0 π = (π Β· π΄) β (βπ β β0 π = (π Β· π΄) β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄)))) |
44 | 43 | impd 412 |
. . . 4
β’ ((πΊ β Mnd β§ π΄ β π΅) β ((βπ β β0 π = (π Β· π΄) β§ βπ β β0 π = (π Β· π΄)) β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄))) |
45 | 2, 3, 7, 1 | cycsubmel 18994 |
. . . . 5
β’ (π β πΆ β βπ β β0 π = (π Β· π΄)) |
46 | 2, 3, 7, 1 | cycsubmel 18994 |
. . . . 5
β’ (π β πΆ β βπ β β0 π = (π Β· π΄)) |
47 | 45, 46 | anbi12i 628 |
. . . 4
β’ ((π β πΆ β§ π β πΆ) β (βπ β β0 π = (π Β· π΄) β§ βπ β β0 π = (π Β· π΄))) |
48 | 2, 3, 7, 1 | cycsubmel 18994 |
. . . 4
β’ ((π(+gβπΊ)π) β πΆ β βπ β β0 (π(+gβπΊ)π) = (π Β· π΄)) |
49 | 44, 47, 48 | 3imtr4g 296 |
. . 3
β’ ((πΊ β Mnd β§ π΄ β π΅) β ((π β πΆ β§ π β πΆ) β (π(+gβπΊ)π) β πΆ)) |
50 | 49 | ralrimivv 3196 |
. 2
β’ ((πΊ β Mnd β§ π΄ β π΅) β βπ β πΆ βπ β πΆ (π(+gβπΊ)π) β πΆ) |
51 | 2, 16, 34 | issubm 18615 |
. . 3
β’ (πΊ β Mnd β (πΆ β (SubMndβπΊ) β (πΆ β π΅ β§ (0gβπΊ) β πΆ β§ βπ β πΆ βπ β πΆ (π(+gβπΊ)π) β πΆ))) |
52 | 51 | adantr 482 |
. 2
β’ ((πΊ β Mnd β§ π΄ β π΅) β (πΆ β (SubMndβπΊ) β (πΆ β π΅ β§ (0gβπΊ) β πΆ β§ βπ β πΆ βπ β πΆ (π(+gβπΊ)π) β πΆ))) |
53 | 10, 22, 50, 52 | mpbir3and 1343 |
1
β’ ((πΊ β Mnd β§ π΄ β π΅) β πΆ β (SubMndβπΊ)) |