Step | Hyp | Ref
| Expression |
1 | | pzriprng.r |
. . . . . . 7
β’ π
= (β€ring
Γs β€ring) |
2 | 1 | pzriprnglem2 21412 |
. . . . . 6
β’
(Baseβπ
) =
(β€ Γ β€) |
3 | 2 | eleq2i 2817 |
. . . . 5
β’ (π₯ β (Baseβπ
) β π₯ β (β€ Γ
β€)) |
4 | | elxp2 5696 |
. . . . 5
β’ (π₯ β (β€ Γ
β€) β βπ
β β€ βπ
β β€ π₯ =
β¨π, πβ©) |
5 | 3, 4 | bitri 274 |
. . . 4
β’ (π₯ β (Baseβπ
) β βπ β β€ βπ β β€ π₯ = β¨π, πβ©) |
6 | | pzriprng.i |
. . . . 5
β’ πΌ = (β€ Γ
{0}) |
7 | 1, 6 | pzriprnglem3 21413 |
. . . 4
β’ (π¦ β πΌ β βπ β β€ π¦ = β¨π, 0β©) |
8 | | simpll 765 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€) β§ π β β€) β π β
β€) |
9 | | simpr 483 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€) β§ π β β€) β π β
β€) |
10 | 8, 9 | zmulcld 12702 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π Β· π) β β€) |
11 | | zcn 12593 |
. . . . . . . . . . . . . . . . 17
β’ (π β β€ β π β
β) |
12 | 11 | adantl 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β€) β π β
β) |
13 | 12 | adantr 479 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β π β
β) |
14 | 13 | mul01d 11443 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π Β· 0) =
0) |
15 | | ovex 7449 |
. . . . . . . . . . . . . . 15
β’ (π Β· 0) β
V |
16 | 15 | elsn 4639 |
. . . . . . . . . . . . . 14
β’ ((π Β· 0) β {0} β
(π Β· 0) =
0) |
17 | 14, 16 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π Β· 0) β
{0}) |
18 | 10, 17 | opelxpd 5711 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β€) β§ π β β€) β
β¨(π Β· π), (π Β· 0)β© β (β€ Γ
{0})) |
19 | 9, 8 | zmulcld 12702 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π Β· π) β β€) |
20 | 13 | mul02d 11442 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€) β§ π β β€) β (0
Β· π) =
0) |
21 | | ovex 7449 |
. . . . . . . . . . . . . . 15
β’ (0
Β· π) β
V |
22 | 21 | elsn 4639 |
. . . . . . . . . . . . . 14
β’ ((0
Β· π) β {0}
β (0 Β· π) =
0) |
23 | 20, 22 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€) β§ π β β€) β (0
Β· π) β
{0}) |
24 | 19, 23 | opelxpd 5711 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β€) β§ π β β€) β
β¨(π Β· π), (0 Β· π)β© β (β€ Γ
{0})) |
25 | | zringbas 21383 |
. . . . . . . . . . . . . . 15
β’ β€ =
(Baseββ€ring) |
26 | | zringring 21379 |
. . . . . . . . . . . . . . . 16
β’
β€ring β Ring |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β
β€ring β Ring) |
28 | | simplr 767 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β π β
β€) |
29 | | 0zd 12600 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β 0 β
β€) |
30 | 28, 29 | zmulcld 12702 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π Β· 0) β
β€) |
31 | | zringmulr 21387 |
. . . . . . . . . . . . . . 15
β’ Β·
= (.rββ€ring) |
32 | | eqid 2725 |
. . . . . . . . . . . . . . 15
β’
(.rβπ
) = (.rβπ
) |
33 | 1, 25, 25, 27, 27, 8, 28, 9, 29, 10, 30, 31, 31, 32 | xpsmul 17556 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€) β§ π β β€) β
(β¨π, πβ©(.rβπ
)β¨π, 0β©) = β¨(π Β· π), (π Β· 0)β©) |
34 | 33 | eleq1d 2810 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€) β§ π β β€) β
((β¨π, πβ©(.rβπ
)β¨π, 0β©) β (β€ Γ {0})
β β¨(π Β·
π), (π Β· 0)β© β (β€ Γ
{0}))) |
35 | | simpl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ (π β β€ β§ π β β€)) β π β
β€) |
36 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ (π β β€ β§ π β β€)) β π β
β€) |
37 | 35, 36 | zmulcld 12702 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ (π β β€ β§ π β β€)) β (π Β· π) β β€) |
38 | 37 | ancoms 457 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π Β· π) β β€) |
39 | | 0zd 12600 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ (π β β€ β§ π β β€)) β 0
β β€) |
40 | | simprr 771 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ (π β β€ β§ π β β€)) β π β
β€) |
41 | 39, 40 | zmulcld 12702 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ (π β β€ β§ π β β€)) β (0
Β· π) β
β€) |
42 | 41 | ancoms 457 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β€) β§ π β β€) β (0
Β· π) β
β€) |
43 | 1, 25, 25, 27, 27, 9, 29, 8, 28, 38, 42, 31, 31, 32 | xpsmul 17556 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€) β§ π β β€) β
(β¨π,
0β©(.rβπ
)β¨π, πβ©) = β¨(π Β· π), (0 Β· π)β©) |
44 | 43 | eleq1d 2810 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€) β§ π β β€) β
((β¨π,
0β©(.rβπ
)β¨π, πβ©) β (β€ Γ {0}) β
β¨(π Β· π), (0 Β· π)β© β (β€ Γ
{0}))) |
45 | 34, 44 | anbi12d 630 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β€) β§ π β β€) β
(((β¨π, πβ©(.rβπ
)β¨π, 0β©) β (β€ Γ {0}) β§
(β¨π,
0β©(.rβπ
)β¨π, πβ©) β (β€ Γ {0})) β
(β¨(π Β· π), (π Β· 0)β© β (β€ Γ
{0}) β§ β¨(π
Β· π), (0 Β·
π)β© β (β€
Γ {0})))) |
46 | 18, 24, 45 | mpbir2and 711 |
. . . . . . . . . . 11
β’ (((π β β€ β§ π β β€) β§ π β β€) β
((β¨π, πβ©(.rβπ
)β¨π, 0β©) β (β€ Γ {0}) β§
(β¨π,
0β©(.rβπ
)β¨π, πβ©) β (β€ Γ
{0}))) |
47 | 46 | adantr 479 |
. . . . . . . . . 10
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β ((β¨π, πβ©(.rβπ
)β¨π, 0β©) β (β€ Γ {0}) β§
(β¨π,
0β©(.rβπ
)β¨π, πβ©) β (β€ Γ
{0}))) |
48 | | oveq12 7425 |
. . . . . . . . . . . . . 14
β’ ((π₯ = β¨π, πβ© β§ π¦ = β¨π, 0β©) β (π₯(.rβπ
)π¦) = (β¨π, πβ©(.rβπ
)β¨π, 0β©)) |
49 | 48 | ancoms 457 |
. . . . . . . . . . . . 13
β’ ((π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©) β (π₯(.rβπ
)π¦) = (β¨π, πβ©(.rβπ
)β¨π, 0β©)) |
50 | 49 | adantl 480 |
. . . . . . . . . . . 12
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β (π₯(.rβπ
)π¦) = (β¨π, πβ©(.rβπ
)β¨π, 0β©)) |
51 | 6 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β πΌ = (β€ Γ {0})) |
52 | 50, 51 | eleq12d 2819 |
. . . . . . . . . . 11
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β ((π₯(.rβπ
)π¦) β πΌ β (β¨π, πβ©(.rβπ
)β¨π, 0β©) β (β€ Γ
{0}))) |
53 | | oveq12 7425 |
. . . . . . . . . . . . 13
β’ ((π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©) β (π¦(.rβπ
)π₯) = (β¨π, 0β©(.rβπ
)β¨π, πβ©)) |
54 | 53 | adantl 480 |
. . . . . . . . . . . 12
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β (π¦(.rβπ
)π₯) = (β¨π, 0β©(.rβπ
)β¨π, πβ©)) |
55 | 54, 51 | eleq12d 2819 |
. . . . . . . . . . 11
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β ((π¦(.rβπ
)π₯) β πΌ β (β¨π, 0β©(.rβπ
)β¨π, πβ©) β (β€ Γ
{0}))) |
56 | 52, 55 | anbi12d 630 |
. . . . . . . . . 10
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β (((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ) β ((β¨π, πβ©(.rβπ
)β¨π, 0β©) β (β€ Γ {0}) β§
(β¨π,
0β©(.rβπ
)β¨π, πβ©) β (β€ Γ
{0})))) |
57 | 47, 56 | mpbird 256 |
. . . . . . . . 9
β’ ((((π β β€ β§ π β β€) β§ π β β€) β§ (π¦ = β¨π, 0β© β§ π₯ = β¨π, πβ©)) β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)) |
58 | 57 | exp32 419 |
. . . . . . . 8
β’ (((π β β€ β§ π β β€) β§ π β β€) β (π¦ = β¨π, 0β© β (π₯ = β¨π, πβ© β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)))) |
59 | 58 | rexlimdva 3145 |
. . . . . . 7
β’ ((π β β€ β§ π β β€) β
(βπ β β€
π¦ = β¨π, 0β© β (π₯ = β¨π, πβ© β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)))) |
60 | 59 | com23 86 |
. . . . . 6
β’ ((π β β€ β§ π β β€) β (π₯ = β¨π, πβ© β (βπ β β€ π¦ = β¨π, 0β© β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)))) |
61 | 60 | rexlimivv 3190 |
. . . . 5
β’
(βπ β
β€ βπ β
β€ π₯ = β¨π, πβ© β (βπ β β€ π¦ = β¨π, 0β© β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ))) |
62 | 61 | imp 405 |
. . . 4
β’
((βπ β
β€ βπ β
β€ π₯ = β¨π, πβ© β§ βπ β β€ π¦ = β¨π, 0β©) β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)) |
63 | 5, 7, 62 | syl2anb 596 |
. . 3
β’ ((π₯ β (Baseβπ
) β§ π¦ β πΌ) β ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)) |
64 | 63 | rgen2 3188 |
. 2
β’
βπ₯ β
(Baseβπ
)βπ¦ β πΌ ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ) |
65 | 1 | pzriprnglem1 21411 |
. . 3
β’ π
β Rng |
66 | 1, 6 | pzriprnglem4 21414 |
. . 3
β’ πΌ β (SubGrpβπ
) |
67 | | eqid 2725 |
. . . 4
β’
(2Idealβπ
) =
(2Idealβπ
) |
68 | | eqid 2725 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
69 | 67, 68, 32 | df2idl2rng 21154 |
. . 3
β’ ((π
β Rng β§ πΌ β (SubGrpβπ
)) β (πΌ β (2Idealβπ
) β βπ₯ β (Baseβπ
)βπ¦ β πΌ ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ))) |
70 | 65, 66, 69 | mp2an 690 |
. 2
β’ (πΌ β (2Idealβπ
) β βπ₯ β (Baseβπ
)βπ¦ β πΌ ((π₯(.rβπ
)π¦) β πΌ β§ (π¦(.rβπ
)π₯) β πΌ)) |
71 | 64, 70 | mpbir 230 |
1
β’ πΌ β (2Idealβπ
) |