Step | Hyp | Ref
| Expression |
1 | | domnring 20766 |
. . . 4
β’ (π
β Domn β π
β Ring) |
2 | 1 | 3ad2ant1 1133 |
. . 3
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π
β Ring) |
3 | | simp2l 1199 |
. . 3
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π β πΏ) |
4 | | simp2r 1200 |
. . 3
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π β { 0 }) |
5 | | lidldomn1.l |
. . . 4
β’ πΏ = (LIdealβπ
) |
6 | | lidldomn1.0 |
. . . 4
β’ 0 =
(0gβπ
) |
7 | 5, 6 | lidlnz 20698 |
. . 3
β’ ((π
β Ring β§ π β πΏ β§ π β { 0 }) β βπ¦ β π π¦ β 0 ) |
8 | 2, 3, 4, 7 | syl3anc 1371 |
. 2
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β βπ¦ β π π¦ β 0 ) |
9 | | oveq2 7365 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (πΌ Β· π₯) = (πΌ Β· π¦)) |
10 | | id 22 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β π₯ = π¦) |
11 | 9, 10 | eqeq12d 2752 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((πΌ Β· π₯) = π₯ β (πΌ Β· π¦) = π¦)) |
12 | | oveq1 7364 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π₯ Β· πΌ) = (π¦ Β· πΌ)) |
13 | 12, 10 | eqeq12d 2752 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π₯ Β· πΌ) = π₯ β (π¦ Β· πΌ) = π¦)) |
14 | 11, 13 | anbi12d 631 |
. . . . . . . . 9
β’ (π₯ = π¦ β (((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β ((πΌ Β· π¦) = π¦ β§ (π¦ Β· πΌ) = π¦))) |
15 | 14 | rspcva 3579 |
. . . . . . . 8
β’ ((π¦ β π β§ βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯)) β ((πΌ Β· π¦) = π¦ β§ (π¦ Β· πΌ) = π¦)) |
16 | 2 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β π
β Ring) |
17 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(Baseβπ
) =
(Baseβπ
) |
18 | 17, 5 | lidlss 20680 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΏ β π β (Baseβπ
)) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β πΏ β§ π β { 0 }) β π β (Baseβπ
)) |
20 | 19 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π β (Baseβπ
)) |
21 | 20 | sseld 3943 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β (π¦ β π β π¦ β (Baseβπ
))) |
22 | 21 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π¦ β (Baseβπ
))) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π β§ π¦ β 0 ) β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π¦ β (Baseβπ
))) |
24 | 23 | impcom 408 |
. . . . . . . . . . . . . 14
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β π¦ β (Baseβπ
)) |
25 | | lidldomn1.t |
. . . . . . . . . . . . . . 15
β’ Β· =
(.rβπ
) |
26 | | lidldomn1.1 |
. . . . . . . . . . . . . . 15
β’ 1 =
(1rβπ
) |
27 | 17, 25, 26 | ringlidm 19992 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π¦ β (Baseβπ
)) β ( 1 Β· π¦) = π¦) |
28 | 16, 24, 27 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ( 1 Β· π¦) = π¦) |
29 | | eqeq2 2748 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = ( 1 Β· π¦) β ((πΌ Β· π¦) = π¦ β (πΌ Β· π¦) = ( 1 Β· π¦))) |
30 | 29 | eqcoms 2744 |
. . . . . . . . . . . . . . 15
β’ (( 1 Β· π¦) = π¦ β ((πΌ Β· π¦) = π¦ β (πΌ Β· π¦) = ( 1 Β· π¦))) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β§ ( 1 Β· π¦) = π¦) β ((πΌ Β· π¦) = π¦ β (πΌ Β· π¦) = ( 1 Β· π¦))) |
32 | | ringgrp 19969 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β Ring β π
β Grp) |
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β Domn β π
β Grp) |
34 | 33 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β π
β Grp) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β π
β Grp) |
36 | 19 | sseld 3943 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β πΏ β§ π β { 0 }) β (πΌ β π β πΌ β (Baseβπ
))) |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β Domn β ((π β πΏ β§ π β { 0 }) β (πΌ β π β πΌ β (Baseβπ
)))) |
38 | 37 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ β (Baseβπ
)) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β πΌ β (Baseβπ
)) |
40 | 17, 25 | ringcl 19981 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β Ring β§ πΌ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΌ Β· π¦) β (Baseβπ
)) |
41 | 16, 39, 24, 40 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (πΌ Β· π¦) β (Baseβπ
)) |
42 | 17, 26 | ringidcl 19989 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β Ring β 1 β
(Baseβπ
)) |
43 | 1, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β Domn β 1 β
(Baseβπ
)) |
44 | 43 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β 1 β (Baseβπ
)) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β 1 β
(Baseβπ
)) |
46 | 17, 25 | ringcl 19981 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β Ring β§ 1 β
(Baseβπ
) β§ π¦ β (Baseβπ
)) β ( 1 Β· π¦) β (Baseβπ
)) |
47 | 16, 45, 24, 46 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ( 1 Β· π¦) β (Baseβπ
)) |
48 | | eqid 2736 |
. . . . . . . . . . . . . . . . . 18
β’
(-gβπ
) = (-gβπ
) |
49 | 17, 6, 48 | grpsubeq0 18833 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Grp β§ (πΌ Β· π¦) β (Baseβπ
) β§ ( 1 Β· π¦) β (Baseβπ
)) β (((πΌ Β· π¦)(-gβπ
)( 1 Β· π¦)) = 0 β (πΌ Β· π¦) = ( 1 Β· π¦))) |
50 | 35, 41, 47, 49 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (((πΌ Β· π¦)(-gβπ
)( 1 Β· π¦)) = 0 β (πΌ Β· π¦) = ( 1 Β· π¦))) |
51 | 17, 25, 48, 16, 39, 45, 24 | ringsubdir 20024 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ((πΌ(-gβπ
) 1 ) Β· π¦) = ((πΌ Β· π¦)(-gβπ
)( 1 Β· π¦))) |
52 | 51 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (((πΌ(-gβπ
) 1 ) Β· π¦) = 0 β ((πΌ Β· π¦)(-gβπ
)( 1 Β· π¦)) = 0 )) |
53 | | simpl1 1191 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β π
β Domn) |
54 | 34, 38, 44 | 3jca 1128 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β (π
β Grp β§ πΌ β (Baseβπ
) β§ 1 β (Baseβπ
))) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (π
β Grp β§ πΌ β (Baseβπ
) β§ 1 β (Baseβπ
))) |
56 | 17, 48 | grpsubcl 18827 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β Grp β§ πΌ β (Baseβπ
) β§ 1 β (Baseβπ
)) β (πΌ(-gβπ
) 1 ) β (Baseβπ
)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (πΌ(-gβπ
) 1 ) β (Baseβπ
)) |
58 | 17, 25, 6 | domneq0 20767 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Domn β§ (πΌ(-gβπ
) 1 ) β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (((πΌ(-gβπ
) 1 ) Β· π¦) = 0 β ((πΌ(-gβπ
) 1 ) = 0 β¨ π¦ = 0 ))) |
59 | 53, 57, 24, 58 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (((πΌ(-gβπ
) 1 ) Β· π¦) = 0 β ((πΌ(-gβπ
) 1 ) = 0 β¨ π¦ = 0 ))) |
60 | 17, 6, 48 | grpsubeq0 18833 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β Grp β§ πΌ β (Baseβπ
) β§ 1 β (Baseβπ
)) β ((πΌ(-gβπ
) 1 ) = 0 β πΌ = 1 )) |
61 | 55, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ((πΌ(-gβπ
) 1 ) = 0 β πΌ = 1 )) |
62 | 61 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ((πΌ(-gβπ
) 1 ) = 0 β πΌ = 1 )) |
63 | | eqneqall 2954 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = 0 β (π¦ β 0 β πΌ = 1 )) |
64 | 63 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β 0 β (π¦ = 0 β πΌ = 1 )) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β π β§ π¦ β 0 ) β (π¦ = 0 β πΌ = 1 )) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (π¦ = 0 β πΌ = 1 )) |
67 | 62, 66 | jaod 857 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (((πΌ(-gβπ
) 1 ) = 0 β¨ π¦ = 0 ) β πΌ = 1 )) |
68 | 59, 67 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (((πΌ(-gβπ
) 1 ) Β· π¦) = 0 β πΌ = 1 )) |
69 | 52, 68 | sylbird 259 |
. . . . . . . . . . . . . . . 16
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β (((πΌ Β· π¦)(-gβπ
)( 1 Β· π¦)) = 0 β πΌ = 1 )) |
70 | 50, 69 | sylbird 259 |
. . . . . . . . . . . . . . 15
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ((πΌ Β· π¦) = ( 1 Β· π¦) β πΌ = 1 )) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β§ ( 1 Β· π¦) = π¦) β ((πΌ Β· π¦) = ( 1 Β· π¦) β πΌ = 1 )) |
72 | 31, 71 | sylbid 239 |
. . . . . . . . . . . . 13
β’ ((((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β§ ( 1 Β· π¦) = π¦) β ((πΌ Β· π¦) = π¦ β πΌ = 1 )) |
73 | 28, 72 | mpdan 685 |
. . . . . . . . . . . 12
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ (π¦ β π β§ π¦ β 0 )) β ((πΌ Β· π¦) = π¦ β πΌ = 1 )) |
74 | 73 | ex 413 |
. . . . . . . . . . 11
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β ((π¦ β π β§ π¦ β 0 ) β ((πΌ Β· π¦) = π¦ β πΌ = 1 ))) |
75 | 74 | com13 88 |
. . . . . . . . . 10
β’ ((πΌ Β· π¦) = π¦ β ((π¦ β π β§ π¦ β 0 ) β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ = 1 ))) |
76 | 75 | expd 416 |
. . . . . . . . 9
β’ ((πΌ Β· π¦) = π¦ β (π¦ β π β (π¦ β 0 β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ = 1 )))) |
77 | 76 | adantr 481 |
. . . . . . . 8
β’ (((πΌ Β· π¦) = π¦ β§ (π¦ Β· πΌ) = π¦) β (π¦ β π β (π¦ β 0 β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ = 1 )))) |
78 | 15, 77 | syl 17 |
. . . . . . 7
β’ ((π¦ β π β§ βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯)) β (π¦ β π β (π¦ β 0 β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ = 1 )))) |
79 | 78 | ex 413 |
. . . . . 6
β’ (π¦ β π β (βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β (π¦ β π β (π¦ β 0 β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ = 1 ))))) |
80 | 79 | pm2.43b 55 |
. . . . 5
β’
(βπ₯ β
π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β (π¦ β π β (π¦ β 0 β ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β πΌ = 1 )))) |
81 | 80 | com14 96 |
. . . 4
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β (π¦ β π β (π¦ β 0 β (βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β πΌ = 1 )))) |
82 | 81 | imp 407 |
. . 3
β’ (((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β§ π¦ β π) β (π¦ β 0 β (βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β πΌ = 1 ))) |
83 | 82 | rexlimdva 3152 |
. 2
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β (βπ¦ β π π¦ β 0 β (βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β πΌ = 1 ))) |
84 | 8, 83 | mpd 15 |
1
β’ ((π
β Domn β§ (π β πΏ β§ π β { 0 }) β§ πΌ β π) β (βπ₯ β π ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯) β πΌ = 1 )) |