Step | Hyp | Ref
| Expression |
1 | | ssdif0 4328 |
. . . 4
β’ (π
β β β (π
β β) =
β
) |
2 | | simpr 486 |
. . . . . 6
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π
β β) β π
β β) |
3 | | simplr 768 |
. . . . . 6
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π
β β) β β β
π
) |
4 | 2, 3 | eqssd 3966 |
. . . . 5
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π
β β) β π
= β) |
5 | 4 | orcd 872 |
. . . 4
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π
β β) β (π
= β β¨ π
= β)) |
6 | 1, 5 | sylan2br 596 |
. . 3
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π
β β) = β
) β (π
= β β¨ π
= β)) |
7 | | n0 4311 |
. . . 4
β’ ((π
β β) β β
β βπ₯ π₯ β (π
β β)) |
8 | | simpll 766 |
. . . . . . . . . 10
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β π
β
(SubRingββfld)) |
9 | | cnfldbas 20816 |
. . . . . . . . . . 11
β’ β =
(Baseββfld) |
10 | 9 | subrgss 20239 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β π
β β) |
11 | 8, 10 | syl 17 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β π
β β) |
12 | | replim 15008 |
. . . . . . . . . . . . 13
β’ (π¦ β β β π¦ = ((ββπ¦) + (i Β·
(ββπ¦)))) |
13 | 12 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β π¦ = ((ββπ¦) + (i Β· (ββπ¦)))) |
14 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β π
β
(SubRingββfld)) |
15 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β β β
π
) |
16 | | recl 15002 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β
(ββπ¦) β
β) |
17 | 16 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β (ββπ¦) β
β) |
18 | 15, 17 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β (ββπ¦) β π
) |
19 | | ax-icn 11117 |
. . . . . . . . . . . . . . . . . . 19
β’ i β
β |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β i β
β) |
21 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π
β β) β π₯ β π
) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β π₯ β π
) |
23 | 11, 22 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β π₯ β β) |
24 | | imcl 15003 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β
(ββπ₯) β
β) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
(ββπ₯) β
β) |
26 | 25 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
(ββπ₯) β
β) |
27 | | eldifn 4092 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π
β β) β Β¬ π₯ β
β) |
28 | 27 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β Β¬ π₯ β
β) |
29 | | reim0b 15011 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β (π₯ β β β
(ββπ₯) =
0)) |
30 | 29 | necon3bbid 2982 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β (Β¬
π₯ β β β
(ββπ₯) β
0)) |
31 | 23, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (Β¬ π₯ β β β
(ββπ₯) β
0)) |
32 | 28, 31 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
(ββπ₯) β
0) |
33 | 20, 26, 32 | divcan4d 11944 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β ((i Β·
(ββπ₯)) /
(ββπ₯)) =
i) |
34 | | mulcl 11142 |
. . . . . . . . . . . . . . . . . . 19
β’ ((i
β β β§ (ββπ₯) β β) β (i Β·
(ββπ₯)) β
β) |
35 | 19, 26, 34 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (i Β·
(ββπ₯)) β
β) |
36 | 35, 26, 32 | divrecd 11941 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β ((i Β·
(ββπ₯)) /
(ββπ₯)) = ((i
Β· (ββπ₯))
Β· (1 / (ββπ₯)))) |
37 | 33, 36 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β i = ((i Β·
(ββπ₯)) Β·
(1 / (ββπ₯)))) |
38 | 23 | recld 15086 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
(ββπ₯) β
β) |
39 | 38 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
(ββπ₯) β
β) |
40 | 23, 39 | negsubd 11525 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (π₯ + -(ββπ₯)) = (π₯ β (ββπ₯))) |
41 | | replim 15008 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β π₯ = ((ββπ₯) + (i Β·
(ββπ₯)))) |
42 | 23, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β π₯ = ((ββπ₯) + (i Β· (ββπ₯)))) |
43 | 42 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (π₯ β (ββπ₯)) = (((ββπ₯) + (i Β·
(ββπ₯))) β
(ββπ₯))) |
44 | 39, 35 | pncan2d 11521 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
(((ββπ₯) + (i
Β· (ββπ₯))) β (ββπ₯)) = (i Β· (ββπ₯))) |
45 | 40, 43, 44 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (π₯ + -(ββπ₯)) = (i Β·
(ββπ₯))) |
46 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β β β
π
) |
47 | 38 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
-(ββπ₯) β
β) |
48 | 46, 47 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β
-(ββπ₯) β
π
) |
49 | | cnfldadd 20817 |
. . . . . . . . . . . . . . . . . . . 20
β’ + =
(+gββfld) |
50 | 49 | subrgacl 20249 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β
(SubRingββfld) β§ π₯ β π
β§ -(ββπ₯) β π
) β (π₯ + -(ββπ₯)) β π
) |
51 | 8, 22, 48, 50 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (π₯ + -(ββπ₯)) β π
) |
52 | 45, 51 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (i Β·
(ββπ₯)) β
π
) |
53 | 25, 32 | rereccld 11989 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (1 /
(ββπ₯)) β
β) |
54 | 46, 53 | sseldd 3950 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (1 /
(ββπ₯)) β
π
) |
55 | | cnfldmul 20818 |
. . . . . . . . . . . . . . . . . 18
β’ Β·
= (.rββfld) |
56 | 55 | subrgmcl 20250 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β
(SubRingββfld) β§ (i Β· (ββπ₯)) β π
β§ (1 / (ββπ₯)) β π
) β ((i Β· (ββπ₯)) Β· (1 /
(ββπ₯))) β
π
) |
57 | 8, 52, 54, 56 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β ((i Β·
(ββπ₯)) Β·
(1 / (ββπ₯)))
β π
) |
58 | 37, 57 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β i β π
) |
59 | 58 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β i β π
) |
60 | | imcl 15003 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β
(ββπ¦) β
β) |
61 | 60 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β (ββπ¦) β
β) |
62 | 15, 61 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β (ββπ¦) β π
) |
63 | 55 | subrgmcl 20250 |
. . . . . . . . . . . . . 14
β’ ((π
β
(SubRingββfld) β§ i β π
β§ (ββπ¦) β π
) β (i Β· (ββπ¦)) β π
) |
64 | 14, 59, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β (i Β·
(ββπ¦)) β
π
) |
65 | 49 | subrgacl 20249 |
. . . . . . . . . . . . 13
β’ ((π
β
(SubRingββfld) β§ (ββπ¦) β π
β§ (i Β· (ββπ¦)) β π
) β ((ββπ¦) + (i Β· (ββπ¦))) β π
) |
66 | 14, 18, 64, 65 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β ((ββπ¦) + (i Β·
(ββπ¦))) β
π
) |
67 | 13, 66 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π₯ β (π
β β) β§ π¦ β β)) β π¦ β π
) |
68 | 67 | expr 458 |
. . . . . . . . . 10
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (π¦ β β β π¦ β π
)) |
69 | 68 | ssrdv 3955 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β β β
π
) |
70 | 11, 69 | eqssd 3966 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β π
= β) |
71 | 70 | olcd 873 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ π₯ β (π
β β)) β (π
= β β¨ π
= β)) |
72 | 71 | ex 414 |
. . . . . 6
β’ ((π
β
(SubRingββfld) β§ β β π
) β (π₯ β (π
β β) β (π
= β β¨ π
= β))) |
73 | 72 | exlimdv 1937 |
. . . . 5
β’ ((π
β
(SubRingββfld) β§ β β π
) β (βπ₯ π₯ β (π
β β) β (π
= β β¨ π
= β))) |
74 | 73 | imp 408 |
. . . 4
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ βπ₯ π₯ β (π
β β)) β (π
= β β¨ π
= β)) |
75 | 7, 74 | sylan2b 595 |
. . 3
β’ (((π
β
(SubRingββfld) β§ β β π
) β§ (π
β β) β β
) β
(π
= β β¨ π
= β)) |
76 | 6, 75 | pm2.61dane 3033 |
. 2
β’ ((π
β
(SubRingββfld) β§ β β π
) β (π
= β β¨ π
= β)) |
77 | | elprg 4612 |
. . 3
β’ (π
β
(SubRingββfld) β (π
β {β, β} β (π
= β β¨ π
= β))) |
78 | 77 | adantr 482 |
. 2
β’ ((π
β
(SubRingββfld) β§ β β π
) β (π
β {β, β} β (π
= β β¨ π
= β))) |
79 | 76, 78 | mpbird 257 |
1
β’ ((π
β
(SubRingββfld) β§ β β π
) β π
β {β, β}) |