Step | Hyp | Ref
| Expression |
1 | | cphsubrglem.k |
. . . . . . . 8
β’ πΎ = (BaseβπΉ) |
2 | | cphsubrglem.1 |
. . . . . . . 8
β’ (π β πΉ = (βfld
βΎs π΄)) |
3 | | cphsubrglem.2 |
. . . . . . . 8
β’ (π β πΉ β DivRing) |
4 | 1, 2, 3 | cphsubrglem 25060 |
. . . . . . 7
β’ (π β (πΉ = (βfld
βΎs πΎ)
β§ πΎ = (π΄ β© β) β§ πΎ β
(SubRingββfld))) |
5 | 4 | simp3d 1141 |
. . . . . 6
β’ (π β πΎ β
(SubRingββfld)) |
6 | 5 | 3ad2ant1 1130 |
. . . . 5
β’ ((π β§ π β πΎ β§ π β 0) β πΎ β
(SubRingββfld)) |
7 | | cnfldbas 21244 |
. . . . . 6
β’ β =
(Baseββfld) |
8 | 7 | subrgss 20474 |
. . . . 5
β’ (πΎ β
(SubRingββfld) β πΎ β β) |
9 | 6, 8 | syl 17 |
. . . 4
β’ ((π β§ π β πΎ β§ π β 0) β πΎ β β) |
10 | | simp2 1134 |
. . . 4
β’ ((π β§ π β πΎ β§ π β 0) β π β πΎ) |
11 | 9, 10 | sseldd 3978 |
. . 3
β’ ((π β§ π β πΎ β§ π β 0) β π β β) |
12 | | simp3 1135 |
. . 3
β’ ((π β§ π β πΎ β§ π β 0) β π β 0) |
13 | | cnfldinv 21291 |
. . 3
β’ ((π β β β§ π β 0) β
((invrββfld)βπ) = (1 / π)) |
14 | 11, 12, 13 | syl2anc 583 |
. 2
β’ ((π β§ π β πΎ β§ π β 0) β
((invrββfld)βπ) = (1 / π)) |
15 | | eqid 2726 |
. . . . . . . . . 10
β’
(βfld βΎs πΎ) = (βfld
βΎs πΎ) |
16 | | cnfld0 21281 |
. . . . . . . . . 10
β’ 0 =
(0gββfld) |
17 | 15, 16 | subrg0 20481 |
. . . . . . . . 9
β’ (πΎ β
(SubRingββfld) β 0 =
(0gβ(βfld βΎs πΎ))) |
18 | 6, 17 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β πΎ β§ π β 0) β 0 =
(0gβ(βfld βΎs πΎ))) |
19 | 4 | simp1d 1139 |
. . . . . . . . . 10
β’ (π β πΉ = (βfld
βΎs πΎ)) |
20 | 19 | 3ad2ant1 1130 |
. . . . . . . . 9
β’ ((π β§ π β πΎ β§ π β 0) β πΉ = (βfld
βΎs πΎ)) |
21 | 20 | fveq2d 6889 |
. . . . . . . 8
β’ ((π β§ π β πΎ β§ π β 0) β (0gβπΉ) =
(0gβ(βfld βΎs πΎ))) |
22 | 18, 21 | eqtr4d 2769 |
. . . . . . 7
β’ ((π β§ π β πΎ β§ π β 0) β 0 =
(0gβπΉ)) |
23 | 12, 22 | neeqtrd 3004 |
. . . . . 6
β’ ((π β§ π β πΎ β§ π β 0) β π β (0gβπΉ)) |
24 | | eldifsn 4785 |
. . . . . 6
β’ (π β (πΎ β {(0gβπΉ)}) β (π β πΎ β§ π β (0gβπΉ))) |
25 | 10, 23, 24 | sylanbrc 582 |
. . . . 5
β’ ((π β§ π β πΎ β§ π β 0) β π β (πΎ β {(0gβπΉ)})) |
26 | 3 | 3ad2ant1 1130 |
. . . . . . 7
β’ ((π β§ π β πΎ β§ π β 0) β πΉ β DivRing) |
27 | | eqid 2726 |
. . . . . . . . 9
β’
(UnitβπΉ) =
(UnitβπΉ) |
28 | | eqid 2726 |
. . . . . . . . 9
β’
(0gβπΉ) = (0gβπΉ) |
29 | 1, 27, 28 | isdrng 20591 |
. . . . . . . 8
β’ (πΉ β DivRing β (πΉ β Ring β§
(UnitβπΉ) = (πΎ β
{(0gβπΉ)}))) |
30 | 29 | simprbi 496 |
. . . . . . 7
β’ (πΉ β DivRing β
(UnitβπΉ) = (πΎ β
{(0gβπΉ)})) |
31 | 26, 30 | syl 17 |
. . . . . 6
β’ ((π β§ π β πΎ β§ π β 0) β (UnitβπΉ) = (πΎ β {(0gβπΉ)})) |
32 | 20 | fveq2d 6889 |
. . . . . 6
β’ ((π β§ π β πΎ β§ π β 0) β (UnitβπΉ) =
(Unitβ(βfld βΎs πΎ))) |
33 | 31, 32 | eqtr3d 2768 |
. . . . 5
β’ ((π β§ π β πΎ β§ π β 0) β (πΎ β {(0gβπΉ)}) =
(Unitβ(βfld βΎs πΎ))) |
34 | 25, 33 | eleqtrd 2829 |
. . . 4
β’ ((π β§ π β πΎ β§ π β 0) β π β (Unitβ(βfld
βΎs πΎ))) |
35 | | eqid 2726 |
. . . . . 6
β’
(Unitββfld) =
(Unitββfld) |
36 | | eqid 2726 |
. . . . . 6
β’
(Unitβ(βfld βΎs πΎ)) = (Unitβ(βfld
βΎs πΎ)) |
37 | | eqid 2726 |
. . . . . 6
β’
(invrββfld) =
(invrββfld) |
38 | 15, 35, 36, 37 | subrgunit 20492 |
. . . . 5
β’ (πΎ β
(SubRingββfld) β (π β (Unitβ(βfld
βΎs πΎ))
β (π β
(Unitββfld) β§ π β πΎ β§
((invrββfld)βπ) β πΎ))) |
39 | 6, 38 | syl 17 |
. . . 4
β’ ((π β§ π β πΎ β§ π β 0) β (π β (Unitβ(βfld
βΎs πΎ))
β (π β
(Unitββfld) β§ π β πΎ β§
((invrββfld)βπ) β πΎ))) |
40 | 34, 39 | mpbid 231 |
. . 3
β’ ((π β§ π β πΎ β§ π β 0) β (π β (Unitββfld)
β§ π β πΎ β§
((invrββfld)βπ) β πΎ)) |
41 | 40 | simp3d 1141 |
. 2
β’ ((π β§ π β πΎ β§ π β 0) β
((invrββfld)βπ) β πΎ) |
42 | 14, 41 | eqeltrrd 2828 |
1
β’ ((π β§ π β πΎ β§ π β 0) β (1 / π) β πΎ) |