Step | Hyp | Ref
| Expression |
1 | | abvpropd.1 |
. . . . 5
β’ (π β π΅ = (BaseβπΎ)) |
2 | | abvpropd.2 |
. . . . 5
β’ (π β π΅ = (BaseβπΏ)) |
3 | | abvpropd.3 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
4 | | abvpropd.4 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) |
5 | 1, 2, 3, 4 | ringpropd 20011 |
. . . 4
β’ (π β (πΎ β Ring β πΏ β Ring)) |
6 | 1, 2 | eqtr3d 2775 |
. . . . . 6
β’ (π β (BaseβπΎ) = (BaseβπΏ)) |
7 | 6 | feq2d 6655 |
. . . . 5
β’ (π β (π:(BaseβπΎ)βΆ(0[,)+β) β π:(BaseβπΏ)βΆ(0[,)+β))) |
8 | 1, 2, 3 | grpidpropd 18522 |
. . . . . . . . . . 11
β’ (π β (0gβπΎ) = (0gβπΏ)) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β (0gβπΎ) = (0gβπΏ)) |
10 | 9 | eqeq2d 2744 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (π₯ = (0gβπΎ) β π₯ = (0gβπΏ))) |
11 | 10 | bibi2d 343 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (((πβπ₯) = 0 β π₯ = (0gβπΎ)) β ((πβπ₯) = 0 β π₯ = (0gβπΏ)))) |
12 | 4 | fveqeq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β (πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
13 | 3 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβ(π₯(+gβπΎ)π¦)) = (πβ(π₯(+gβπΏ)π¦))) |
14 | 13 | breq1d 5116 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) |
15 | 12, 14 | anbi12d 632 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
16 | 15 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β π΅) β (((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
17 | 16 | ralbidva 3169 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (βπ¦ β π΅ ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β π΅ ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
18 | 11, 17 | anbi12d 632 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β (((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
19 | 18 | ralbidva 3169 |
. . . . . 6
β’ (π β (βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
20 | 1 | raleqdv 3312 |
. . . . . . . 8
β’ (π β (βπ¦ β π΅ ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
21 | 20 | anbi2d 630 |
. . . . . . 7
β’ (π β ((((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β (((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
22 | 1, 21 | raleqbidv 3318 |
. . . . . 6
β’ (π β (βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β βπ₯ β (BaseβπΎ)(((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
23 | 2 | raleqdv 3312 |
. . . . . . . 8
β’ (π β (βπ¦ β π΅ ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
24 | 23 | anbi2d 630 |
. . . . . . 7
β’ (π β ((((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β (((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
25 | 2, 24 | raleqbidv 3318 |
. . . . . 6
β’ (π β (βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β π΅ ((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β βπ₯ β (BaseβπΏ)(((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
26 | 19, 22, 25 | 3bitr3d 309 |
. . . . 5
β’ (π β (βπ₯ β (BaseβπΎ)(((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β βπ₯ β (BaseβπΏ)(((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
27 | 7, 26 | anbi12d 632 |
. . . 4
β’ (π β ((π:(BaseβπΎ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΎ)(((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))))) β (π:(BaseβπΏ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΏ)(((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))))) |
28 | 5, 27 | anbi12d 632 |
. . 3
β’ (π β ((πΎ β Ring β§ (π:(BaseβπΎ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΎ)(((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))) β (πΏ β Ring β§ (π:(BaseβπΏ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΏ)(((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦)))))))) |
29 | | eqid 2733 |
. . . . 5
β’
(AbsValβπΎ) =
(AbsValβπΎ) |
30 | 29 | abvrcl 20294 |
. . . 4
β’ (π β (AbsValβπΎ) β πΎ β Ring) |
31 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
32 | | eqid 2733 |
. . . . 5
β’
(+gβπΎ) = (+gβπΎ) |
33 | | eqid 2733 |
. . . . 5
β’
(.rβπΎ) = (.rβπΎ) |
34 | | eqid 2733 |
. . . . 5
β’
(0gβπΎ) = (0gβπΎ) |
35 | 29, 31, 32, 33, 34 | isabv 20292 |
. . . 4
β’ (πΎ β Ring β (π β (AbsValβπΎ) β (π:(BaseβπΎ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΎ)(((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))))))) |
36 | 30, 35 | biadanii 821 |
. . 3
β’ (π β (AbsValβπΎ) β (πΎ β Ring β§ (π:(BaseβπΎ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΎ)(((πβπ₯) = 0 β π₯ = (0gβπΎ)) β§ βπ¦ β (BaseβπΎ)((πβ(π₯(.rβπΎ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΎ)π¦)) β€ ((πβπ₯) + (πβπ¦))))))) |
37 | | eqid 2733 |
. . . . 5
β’
(AbsValβπΏ) =
(AbsValβπΏ) |
38 | 37 | abvrcl 20294 |
. . . 4
β’ (π β (AbsValβπΏ) β πΏ β Ring) |
39 | | eqid 2733 |
. . . . 5
β’
(BaseβπΏ) =
(BaseβπΏ) |
40 | | eqid 2733 |
. . . . 5
β’
(+gβπΏ) = (+gβπΏ) |
41 | | eqid 2733 |
. . . . 5
β’
(.rβπΏ) = (.rβπΏ) |
42 | | eqid 2733 |
. . . . 5
β’
(0gβπΏ) = (0gβπΏ) |
43 | 37, 39, 40, 41, 42 | isabv 20292 |
. . . 4
β’ (πΏ β Ring β (π β (AbsValβπΏ) β (π:(BaseβπΏ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΏ)(((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))))) |
44 | 38, 43 | biadanii 821 |
. . 3
β’ (π β (AbsValβπΏ) β (πΏ β Ring β§ (π:(BaseβπΏ)βΆ(0[,)+β) β§ βπ₯ β (BaseβπΏ)(((πβπ₯) = 0 β π₯ = (0gβπΏ)) β§ βπ¦ β (BaseβπΏ)((πβ(π₯(.rβπΏ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπΏ)π¦)) β€ ((πβπ₯) + (πβπ¦))))))) |
45 | 28, 36, 44 | 3bitr4g 314 |
. 2
β’ (π β (π β (AbsValβπΎ) β π β (AbsValβπΏ))) |
46 | 45 | eqrdv 2731 |
1
β’ (π β (AbsValβπΎ) = (AbsValβπΏ)) |