Step | Hyp | Ref
| Expression |
1 | | rng2idlring.r |
. . . 4
β’ (π β π
β Rng) |
2 | 1 | 3ad2ant1 1131 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β π
β Rng) |
3 | | rng2idlring.i |
. . . . 5
β’ (π β πΌ β (2Idealβπ
)) |
4 | | rng2idlring.j |
. . . . 5
β’ π½ = (π
βΎs πΌ) |
5 | | rng2idlring.u |
. . . . 5
β’ (π β π½ β Ring) |
6 | | rng2idlring.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
7 | | rng2idlring.t |
. . . . 5
β’ Β· =
(.rβπ
) |
8 | | rng2idlring.1 |
. . . . 5
β’ 1 =
(1rβπ½) |
9 | 1, 3, 4, 5, 6, 7, 8 | rngqiprng1elbas 21165 |
. . . 4
β’ (π β 1 β π΅) |
10 | 9 | 3ad2ant1 1131 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β 1 β π΅) |
11 | | rnggrp 20089 |
. . . . . 6
β’ (π
β Rng β π
β Grp) |
12 | 1, 11 | syl 17 |
. . . . 5
β’ (π β π
β Grp) |
13 | 12 | 3ad2ant1 1131 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β π
β Grp) |
14 | | simp3 1136 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β πΆ β π΅) |
15 | 6, 7 | rngcl 20095 |
. . . . 5
β’ ((π
β Rng β§ 1 β π΅ β§ πΆ β π΅) β ( 1 Β· πΆ) β π΅) |
16 | 2, 10, 14, 15 | syl3anc 1369 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· πΆ) β π΅) |
17 | | eqid 2727 |
. . . . 5
β’
(-gβπ
) = (-gβπ
) |
18 | 6, 17 | grpsubcl 18967 |
. . . 4
β’ ((π
β Grp β§ πΆ β π΅ β§ ( 1 Β· πΆ) β π΅) β (πΆ(-gβπ
)( 1 Β· πΆ)) β π΅) |
19 | 13, 14, 16, 18 | syl3anc 1369 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β (πΆ(-gβπ
)( 1 Β· πΆ)) β π΅) |
20 | | eqid 2727 |
. . . . . . 7
β’
(2Idealβπ
) =
(2Idealβπ
) |
21 | 6, 20 | 2idlss 21145 |
. . . . . 6
β’ (πΌ β (2Idealβπ
) β πΌ β π΅) |
22 | 3, 21 | syl 17 |
. . . . 5
β’ (π β πΌ β π΅) |
23 | 22 | sselda 3978 |
. . . 4
β’ ((π β§ π΄ β πΌ) β π΄ β π΅) |
24 | 23 | 3adant3 1130 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β π΄ β π΅) |
25 | | eqid 2727 |
. . . 4
β’
(+gβπ
) = (+gβπ
) |
26 | 6, 25, 7 | rngdi 20091 |
. . 3
β’ ((π
β Rng β§ ( 1 β π΅ β§ (πΆ(-gβπ
)( 1 Β· πΆ)) β π΅ β§ π΄ β π΅)) β ( 1 Β· ((πΆ(-gβπ
)( 1 Β· πΆ))(+gβπ
)π΄)) = (( 1 Β· (πΆ(-gβπ
)( 1 Β· πΆ)))(+gβπ
)( 1 Β· π΄))) |
27 | 2, 10, 19, 24, 26 | syl13anc 1370 |
. 2
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· ((πΆ(-gβπ
)( 1 Β· πΆ))(+gβπ
)π΄)) = (( 1 Β· (πΆ(-gβπ
)( 1 Β· πΆ)))(+gβπ
)( 1 Β· π΄))) |
28 | 6, 7, 17, 2, 10, 14, 16 | rngsubdi 20102 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· (πΆ(-gβπ
)( 1 Β· πΆ))) = (( 1 Β· πΆ)(-gβπ
)( 1 Β· ( 1 Β· πΆ)))) |
29 | 4, 7 | ressmulr 17279 |
. . . . . . . . 9
β’ (πΌ β (2Idealβπ
) β Β· =
(.rβπ½)) |
30 | 3, 29 | syl 17 |
. . . . . . . 8
β’ (π β Β· =
(.rβπ½)) |
31 | 30 | oveqd 7431 |
. . . . . . 7
β’ (π β ( 1 Β· ( 1 Β· πΆ)) = ( 1 (.rβπ½)( 1 Β· πΆ))) |
32 | 31 | 3ad2ant1 1131 |
. . . . . 6
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· ( 1 Β· πΆ)) = ( 1 (.rβπ½)( 1 Β· πΆ))) |
33 | | eqid 2727 |
. . . . . . 7
β’
(Baseβπ½) =
(Baseβπ½) |
34 | | eqid 2727 |
. . . . . . 7
β’
(.rβπ½) = (.rβπ½) |
35 | 5 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β π½ β Ring) |
36 | 1, 3, 4, 5, 6, 7, 8 | rngqiprngghmlem1 21166 |
. . . . . . . 8
β’ ((π β§ πΆ β π΅) β ( 1 Β· πΆ) β (Baseβπ½)) |
37 | 36 | 3adant2 1129 |
. . . . . . 7
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· πΆ) β (Baseβπ½)) |
38 | 33, 34, 8, 35, 37 | ringlidmd 20197 |
. . . . . 6
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 (.rβπ½)( 1 Β· πΆ)) = ( 1 Β· πΆ)) |
39 | 32, 38 | eqtrd 2767 |
. . . . 5
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· ( 1 Β· πΆ)) = ( 1 Β· πΆ)) |
40 | 39 | oveq2d 7430 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β (( 1 Β· πΆ)(-gβπ
)( 1 Β· ( 1 Β· πΆ))) = (( 1 Β· πΆ)(-gβπ
)( 1 Β· πΆ))) |
41 | | eqid 2727 |
. . . . . 6
β’
(0gβπ
) = (0gβπ
) |
42 | 6, 41, 17 | grpsubid 18971 |
. . . . 5
β’ ((π
β Grp β§ ( 1 Β· πΆ) β π΅) β (( 1 Β· πΆ)(-gβπ
)( 1 Β· πΆ)) = (0gβπ
)) |
43 | 13, 16, 42 | syl2anc 583 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β (( 1 Β· πΆ)(-gβπ
)( 1 Β· πΆ)) = (0gβπ
)) |
44 | 28, 40, 43 | 3eqtrd 2771 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· (πΆ(-gβπ
)( 1 Β· πΆ))) = (0gβπ
)) |
45 | 44 | oveq1d 7429 |
. 2
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β (( 1 Β· (πΆ(-gβπ
)( 1 Β· πΆ)))(+gβπ
)( 1 Β· π΄)) = ((0gβπ
)(+gβπ
)( 1 Β· π΄))) |
46 | 6, 7 | rngcl 20095 |
. . . . 5
β’ ((π
β Rng β§ 1 β π΅ β§ π΄ β π΅) β ( 1 Β· π΄) β π΅) |
47 | 2, 10, 24, 46 | syl3anc 1369 |
. . . 4
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· π΄) β π΅) |
48 | 6, 25, 41, 13, 47 | grplidd 18917 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ((0gβπ
)(+gβπ
)( 1 Β· π΄)) = ( 1 Β· π΄)) |
49 | 30 | oveqd 7431 |
. . . 4
β’ (π β ( 1 Β· π΄) = ( 1 (.rβπ½)π΄)) |
50 | 49 | 3ad2ant1 1131 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· π΄) = ( 1 (.rβπ½)π΄)) |
51 | 5 | adantr 480 |
. . . . 5
β’ ((π β§ π΄ β πΌ) β π½ β Ring) |
52 | 3, 4, 33 | 2idlbas 21146 |
. . . . . . . 8
β’ (π β (Baseβπ½) = πΌ) |
53 | 52 | eqcomd 2733 |
. . . . . . 7
β’ (π β πΌ = (Baseβπ½)) |
54 | 53 | eleq2d 2814 |
. . . . . 6
β’ (π β (π΄ β πΌ β π΄ β (Baseβπ½))) |
55 | 54 | biimpa 476 |
. . . . 5
β’ ((π β§ π΄ β πΌ) β π΄ β (Baseβπ½)) |
56 | 33, 34, 8, 51, 55 | ringlidmd 20197 |
. . . 4
β’ ((π β§ π΄ β πΌ) β ( 1 (.rβπ½)π΄) = π΄) |
57 | 56 | 3adant3 1130 |
. . 3
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 (.rβπ½)π΄) = π΄) |
58 | 48, 50, 57 | 3eqtrd 2771 |
. 2
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ((0gβπ
)(+gβπ
)( 1 Β· π΄)) = π΄) |
59 | 27, 45, 58 | 3eqtrd 2771 |
1
β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· ((πΆ(-gβπ
)( 1 Β· πΆ))(+gβπ
)π΄)) = π΄) |