Step | Hyp | Ref
| Expression |
1 | | abvres.b |
. . 3
β’ π΅ = (AbsValβπ) |
2 | 1 | a1i 11 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β π΅ = (AbsValβπ)) |
3 | | abvres.s |
. . . 4
β’ π = (π
βΎs πΆ) |
4 | 3 | subrgbas 20328 |
. . 3
β’ (πΆ β (SubRingβπ
) β πΆ = (Baseβπ)) |
5 | 4 | adantl 483 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β πΆ = (Baseβπ)) |
6 | | eqid 2733 |
. . . 4
β’
(+gβπ
) = (+gβπ
) |
7 | 3, 6 | ressplusg 17235 |
. . 3
β’ (πΆ β (SubRingβπ
) β
(+gβπ
) =
(+gβπ)) |
8 | 7 | adantl 483 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β (+gβπ
) = (+gβπ)) |
9 | | eqid 2733 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
10 | 3, 9 | ressmulr 17252 |
. . 3
β’ (πΆ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
11 | 10 | adantl 483 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β (.rβπ
) = (.rβπ)) |
12 | | subrgsubg 20325 |
. . . 4
β’ (πΆ β (SubRingβπ
) β πΆ β (SubGrpβπ
)) |
13 | 12 | adantl 483 |
. . 3
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β πΆ β (SubGrpβπ
)) |
14 | | eqid 2733 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
15 | 3, 14 | subg0 19012 |
. . 3
β’ (πΆ β (SubGrpβπ
) β
(0gβπ
) =
(0gβπ)) |
16 | 13, 15 | syl 17 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β (0gβπ
) = (0gβπ)) |
17 | 3 | subrgring 20322 |
. . 3
β’ (πΆ β (SubRingβπ
) β π β Ring) |
18 | 17 | adantl 483 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β π β Ring) |
19 | | abvres.a |
. . . 4
β’ π΄ = (AbsValβπ
) |
20 | | eqid 2733 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
21 | 19, 20 | abvf 20431 |
. . 3
β’ (πΉ β π΄ β πΉ:(Baseβπ
)βΆβ) |
22 | 20 | subrgss 20320 |
. . 3
β’ (πΆ β (SubRingβπ
) β πΆ β (Baseβπ
)) |
23 | | fssres 6758 |
. . 3
β’ ((πΉ:(Baseβπ
)βΆβ β§ πΆ β (Baseβπ
)) β (πΉ βΎ πΆ):πΆβΆβ) |
24 | 21, 22, 23 | syl2an 597 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β (πΉ βΎ πΆ):πΆβΆβ) |
25 | 14 | subg0cl 19014 |
. . . 4
β’ (πΆ β (SubGrpβπ
) β
(0gβπ
)
β πΆ) |
26 | | fvres 6911 |
. . . 4
β’
((0gβπ
) β πΆ β ((πΉ βΎ πΆ)β(0gβπ
)) = (πΉβ(0gβπ
))) |
27 | 13, 25, 26 | 3syl 18 |
. . 3
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β ((πΉ βΎ πΆ)β(0gβπ
)) = (πΉβ(0gβπ
))) |
28 | 19, 14 | abv0 20439 |
. . . 4
β’ (πΉ β π΄ β (πΉβ(0gβπ
)) = 0) |
29 | 28 | adantr 482 |
. . 3
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β (πΉβ(0gβπ
)) = 0) |
30 | 27, 29 | eqtrd 2773 |
. 2
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β ((πΉ βΎ πΆ)β(0gβπ
)) = 0) |
31 | | simp1l 1198 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ β§ π₯ β (0gβπ
)) β πΉ β π΄) |
32 | 22 | adantl 483 |
. . . . . 6
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β πΆ β (Baseβπ
)) |
33 | 32 | sselda 3983 |
. . . . 5
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ) β π₯ β (Baseβπ
)) |
34 | 33 | 3adant3 1133 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ β§ π₯ β (0gβπ
)) β π₯ β (Baseβπ
)) |
35 | | simp3 1139 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ β§ π₯ β (0gβπ
)) β π₯ β (0gβπ
)) |
36 | 19, 20, 14 | abvgt0 20436 |
. . . 4
β’ ((πΉ β π΄ β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β 0 < (πΉβπ₯)) |
37 | 31, 34, 35, 36 | syl3anc 1372 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ β§ π₯ β (0gβπ
)) β 0 < (πΉβπ₯)) |
38 | | fvres 6911 |
. . . 4
β’ (π₯ β πΆ β ((πΉ βΎ πΆ)βπ₯) = (πΉβπ₯)) |
39 | 38 | 3ad2ant2 1135 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ β§ π₯ β (0gβπ
)) β ((πΉ βΎ πΆ)βπ₯) = (πΉβπ₯)) |
40 | 37, 39 | breqtrrd 5177 |
. 2
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ π₯ β πΆ β§ π₯ β (0gβπ
)) β 0 < ((πΉ βΎ πΆ)βπ₯)) |
41 | | simp1l 1198 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β πΉ β π΄) |
42 | | simp1r 1199 |
. . . . . 6
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β πΆ β (SubRingβπ
)) |
43 | 42, 22 | syl 17 |
. . . . 5
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β πΆ β (Baseβπ
)) |
44 | | simp2l 1200 |
. . . . 5
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β π₯ β πΆ) |
45 | 43, 44 | sseldd 3984 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β π₯ β (Baseβπ
)) |
46 | | simp3l 1202 |
. . . . 5
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β π¦ β πΆ) |
47 | 43, 46 | sseldd 3984 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β π¦ β (Baseβπ
)) |
48 | 19, 20, 9 | abvmul 20437 |
. . . 4
β’ ((πΉ β π΄ β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
49 | 41, 45, 47, 48 | syl3anc 1372 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β (πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
50 | 9 | subrgmcl 20331 |
. . . . 5
β’ ((πΆ β (SubRingβπ
) β§ π₯ β πΆ β§ π¦ β πΆ) β (π₯(.rβπ
)π¦) β πΆ) |
51 | 42, 44, 46, 50 | syl3anc 1372 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β (π₯(.rβπ
)π¦) β πΆ) |
52 | 51 | fvresd 6912 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β ((πΉ βΎ πΆ)β(π₯(.rβπ
)π¦)) = (πΉβ(π₯(.rβπ
)π¦))) |
53 | 44 | fvresd 6912 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β ((πΉ βΎ πΆ)βπ₯) = (πΉβπ₯)) |
54 | 46 | fvresd 6912 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β ((πΉ βΎ πΆ)βπ¦) = (πΉβπ¦)) |
55 | 53, 54 | oveq12d 7427 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β (((πΉ βΎ πΆ)βπ₯) Β· ((πΉ βΎ πΆ)βπ¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
56 | 49, 52, 55 | 3eqtr4d 2783 |
. 2
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β ((πΉ βΎ πΆ)β(π₯(.rβπ
)π¦)) = (((πΉ βΎ πΆ)βπ₯) Β· ((πΉ βΎ πΆ)βπ¦))) |
57 | 19, 20, 6 | abvtri 20438 |
. . . 4
β’ ((πΉ β π΄ β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
58 | 41, 45, 47, 57 | syl3anc 1372 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
59 | 6 | subrgacl 20330 |
. . . . 5
β’ ((πΆ β (SubRingβπ
) β§ π₯ β πΆ β§ π¦ β πΆ) β (π₯(+gβπ
)π¦) β πΆ) |
60 | 42, 44, 46, 59 | syl3anc 1372 |
. . . 4
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β (π₯(+gβπ
)π¦) β πΆ) |
61 | 60 | fvresd 6912 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β ((πΉ βΎ πΆ)β(π₯(+gβπ
)π¦)) = (πΉβ(π₯(+gβπ
)π¦))) |
62 | 53, 54 | oveq12d 7427 |
. . 3
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β (((πΉ βΎ πΆ)βπ₯) + ((πΉ βΎ πΆ)βπ¦)) = ((πΉβπ₯) + (πΉβπ¦))) |
63 | 58, 61, 62 | 3brtr4d 5181 |
. 2
β’ (((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β§ (π₯ β πΆ β§ π₯ β (0gβπ
)) β§ (π¦ β πΆ β§ π¦ β (0gβπ
))) β ((πΉ βΎ πΆ)β(π₯(+gβπ
)π¦)) β€ (((πΉ βΎ πΆ)βπ₯) + ((πΉ βΎ πΆ)βπ¦))) |
64 | 2, 5, 8, 11, 16, 18, 24, 30, 40, 56, 63 | isabvd 20428 |
1
β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ
)) β (πΉ βΎ πΆ) β π΅) |