Step | Hyp | Ref
| Expression |
1 | | inss2 4190 |
. . . 4
β’ (πΌ β© π΄) β π΄ |
2 | | idlinsubrg.s |
. . . . 5
β’ π = (π
βΎs π΄) |
3 | 2 | subrgbas 20245 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
4 | 1, 3 | sseqtrid 3997 |
. . 3
β’ (π΄ β (SubRingβπ
) β (πΌ β© π΄) β (Baseβπ)) |
5 | 4 | adantr 482 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (πΌ β© π΄) β (Baseβπ)) |
6 | | subrgrcl 20241 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
7 | | idlinsubrg.u |
. . . . . 6
β’ π = (LIdealβπ
) |
8 | | eqid 2733 |
. . . . . 6
β’
(0gβπ
) = (0gβπ
) |
9 | 7, 8 | lidl0cl 20698 |
. . . . 5
β’ ((π
β Ring β§ πΌ β π) β (0gβπ
) β πΌ) |
10 | 6, 9 | sylan 581 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (0gβπ
) β πΌ) |
11 | | subrgsubg 20242 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π΄ β (SubGrpβπ
)) |
12 | | subgsubm 18955 |
. . . . . 6
β’ (π΄ β (SubGrpβπ
) β π΄ β (SubMndβπ
)) |
13 | 8 | subm0cl 18627 |
. . . . . 6
β’ (π΄ β (SubMndβπ
) β
(0gβπ
)
β π΄) |
14 | 11, 12, 13 | 3syl 18 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(0gβπ
)
β π΄) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (0gβπ
) β π΄) |
16 | 10, 15 | elind 4155 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (0gβπ
) β (πΌ β© π΄)) |
17 | 16 | ne0d 4296 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (πΌ β© π΄) β β
) |
18 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ
) = (+gβπ
) |
19 | 2, 18 | ressplusg 17176 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(+gβπ
) =
(+gβπ)) |
20 | | eqid 2733 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
21 | 2, 20 | ressmulr 17193 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
22 | 21 | oveqd 7375 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β (π₯(.rβπ
)π) = (π₯(.rβπ)π)) |
23 | | eqidd 2734 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β π = π) |
24 | 19, 22, 23 | oveq123d 7379 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β ((π₯(.rβπ
)π)(+gβπ
)π) = ((π₯(.rβπ)π)(+gβπ)π)) |
25 | 24 | ad4antr 731 |
. . . . . 6
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β ((π₯(.rβπ
)π)(+gβπ
)π) = ((π₯(.rβπ)π)(+gβπ)π)) |
26 | 6 | ad4antr 731 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π
β Ring) |
27 | | simp-4r 783 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β πΌ β π) |
28 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβπ
) =
(Baseβπ
) |
29 | 28 | subrgss 20237 |
. . . . . . . . . . . . 13
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
30 | 3, 29 | eqsstrrd 3984 |
. . . . . . . . . . . 12
β’ (π΄ β (SubRingβπ
) β (Baseβπ) β (Baseβπ
)) |
31 | 30 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (Baseβπ) β (Baseβπ
)) |
32 | 31 | sselda 3945 |
. . . . . . . . . 10
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ
)) |
33 | 32 | ad2antrr 725 |
. . . . . . . . 9
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π₯ β (Baseβπ
)) |
34 | | inss1 4189 |
. . . . . . . . . . . 12
β’ (πΌ β© π΄) β πΌ |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β (πΌ β© π΄) β πΌ) |
36 | 35 | sselda 3945 |
. . . . . . . . . 10
β’ ((((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β π β πΌ) |
37 | 36 | adantr 482 |
. . . . . . . . 9
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π β πΌ) |
38 | 7, 28, 20 | lidlmcl 20703 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΌ β π) β§ (π₯ β (Baseβπ
) β§ π β πΌ)) β (π₯(.rβπ
)π) β πΌ) |
39 | 26, 27, 33, 37, 38 | syl22anc 838 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β (π₯(.rβπ
)π) β πΌ) |
40 | 34 | a1i 11 |
. . . . . . . . 9
β’ ((((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β (πΌ β© π΄) β πΌ) |
41 | 40 | sselda 3945 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π β πΌ) |
42 | 7, 18 | lidlacl 20699 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β π) β§ ((π₯(.rβπ
)π) β πΌ β§ π β πΌ)) β ((π₯(.rβπ
)π)(+gβπ
)π) β πΌ) |
43 | 26, 27, 39, 41, 42 | syl22anc 838 |
. . . . . . 7
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β ((π₯(.rβπ
)π)(+gβπ
)π) β πΌ) |
44 | | simp-4l 782 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π΄ β (SubRingβπ
)) |
45 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ)) |
46 | 3 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β π΄ = (Baseβπ)) |
47 | 45, 46 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β π₯ β π΄) |
48 | 47 | ad2antrr 725 |
. . . . . . . . 9
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π₯ β π΄) |
49 | 1 | a1i 11 |
. . . . . . . . . . 11
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β (πΌ β© π΄) β π΄) |
50 | 49 | sselda 3945 |
. . . . . . . . . 10
β’ ((((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β π β π΄) |
51 | 50 | adantr 482 |
. . . . . . . . 9
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π β π΄) |
52 | 20 | subrgmcl 20248 |
. . . . . . . . 9
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π΄ β§ π β π΄) β (π₯(.rβπ
)π) β π΄) |
53 | 44, 48, 51, 52 | syl3anc 1372 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β (π₯(.rβπ
)π) β π΄) |
54 | 1 | a1i 11 |
. . . . . . . . 9
β’ ((((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β (πΌ β© π΄) β π΄) |
55 | 54 | sselda 3945 |
. . . . . . . 8
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β π β π΄) |
56 | 18 | subrgacl 20247 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ (π₯(.rβπ
)π) β π΄ β§ π β π΄) β ((π₯(.rβπ
)π)(+gβπ
)π) β π΄) |
57 | 44, 53, 55, 56 | syl3anc 1372 |
. . . . . . 7
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β ((π₯(.rβπ
)π)(+gβπ
)π) β π΄) |
58 | 43, 57 | elind 4155 |
. . . . . 6
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β ((π₯(.rβπ
)π)(+gβπ
)π) β (πΌ β© π΄)) |
59 | 25, 58 | eqeltrrd 2835 |
. . . . 5
β’
(((((π΄ β
(SubRingβπ
) β§
πΌ β π) β§ π₯ β (Baseβπ)) β§ π β (πΌ β© π΄)) β§ π β (πΌ β© π΄)) β ((π₯(.rβπ)π)(+gβπ)π) β (πΌ β© π΄)) |
60 | 59 | anasss 468 |
. . . 4
β’ ((((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β§ (π β (πΌ β© π΄) β§ π β (πΌ β© π΄))) β ((π₯(.rβπ)π)(+gβπ)π) β (πΌ β© π΄)) |
61 | 60 | ralrimivva 3194 |
. . 3
β’ (((π΄ β (SubRingβπ
) β§ πΌ β π) β§ π₯ β (Baseβπ)) β βπ β (πΌ β© π΄)βπ β (πΌ β© π΄)((π₯(.rβπ)π)(+gβπ)π) β (πΌ β© π΄)) |
62 | 61 | ralrimiva 3140 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β βπ₯ β (Baseβπ)βπ β (πΌ β© π΄)βπ β (πΌ β© π΄)((π₯(.rβπ)π)(+gβπ)π) β (πΌ β© π΄)) |
63 | | idlinsubrg.v |
. . 3
β’ π = (LIdealβπ) |
64 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
65 | | eqid 2733 |
. . 3
β’
(+gβπ) = (+gβπ) |
66 | | eqid 2733 |
. . 3
β’
(.rβπ) = (.rβπ) |
67 | 63, 64, 65, 66 | islidl 20697 |
. 2
β’ ((πΌ β© π΄) β π β ((πΌ β© π΄) β (Baseβπ) β§ (πΌ β© π΄) β β
β§ βπ₯ β (Baseβπ)βπ β (πΌ β© π΄)βπ β (πΌ β© π΄)((π₯(.rβπ)π)(+gβπ)π) β (πΌ β© π΄))) |
68 | 5, 17, 62, 67 | syl3anbrc 1344 |
1
β’ ((π΄ β (SubRingβπ
) β§ πΌ β π) β (πΌ β© π΄) β π) |