Step | Hyp | Ref
| Expression |
1 | | simp3 1138 |
. . . . . . 7
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β πΆ β (LIdealβπ
)) |
2 | 1 | sselda 3942 |
. . . . . 6
β’ (((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β§ π β πΆ) β π β (LIdealβπ
)) |
3 | | eqid 2736 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
4 | | eqid 2736 |
. . . . . . 7
β’
(LIdealβπ
) =
(LIdealβπ
) |
5 | 3, 4 | lidlss 20665 |
. . . . . 6
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
6 | 2, 5 | syl 17 |
. . . . 5
β’ (((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β§ π β πΆ) β π β (Baseβπ
)) |
7 | 6 | ralrimiva 3141 |
. . . 4
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β βπ β πΆ π β (Baseβπ
)) |
8 | | pwssb 5059 |
. . . 4
β’ (πΆ β π«
(Baseβπ
) β
βπ β πΆ π β (Baseβπ
)) |
9 | 7, 8 | sylibr 233 |
. . 3
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β πΆ β π« (Baseβπ
)) |
10 | | simp2 1137 |
. . 3
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β πΆ β β
) |
11 | | intss2 5066 |
. . . 4
β’ (πΆ β π«
(Baseβπ
) β
(πΆ β β
β
β© πΆ β (Baseβπ
))) |
12 | 11 | imp 407 |
. . 3
β’ ((πΆ β π«
(Baseβπ
) β§ πΆ β β
) β β© πΆ
β (Baseβπ
)) |
13 | 9, 10, 12 | syl2anc 584 |
. 2
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β β© πΆ
β (Baseβπ
)) |
14 | | simpl1 1191 |
. . . . . 6
β’ (((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β§ π β πΆ) β π
β Ring) |
15 | | eqid 2736 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
16 | 4, 15 | lidl0cl 20667 |
. . . . . 6
β’ ((π
β Ring β§ π β (LIdealβπ
)) β
(0gβπ
)
β π) |
17 | 14, 2, 16 | syl2anc 584 |
. . . . 5
β’ (((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β§ π β πΆ) β (0gβπ
) β π) |
18 | 17 | ralrimiva 3141 |
. . . 4
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β βπ β πΆ (0gβπ
) β π) |
19 | | fvex 6852 |
. . . . 5
β’
(0gβπ
) β V |
20 | 19 | elint2 4912 |
. . . 4
β’
((0gβπ
) β β© πΆ β βπ β πΆ (0gβπ
) β π) |
21 | 18, 20 | sylibr 233 |
. . 3
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β
(0gβπ
)
β β© πΆ) |
22 | 21 | ne0d 4293 |
. 2
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β β© πΆ
β β
) |
23 | 14 | ad5ant15 757 |
. . . . . . . 8
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π
β Ring) |
24 | 2 | ad5ant15 757 |
. . . . . . . 8
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π β (LIdealβπ
)) |
25 | | simp-4r 782 |
. . . . . . . . 9
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π₯ β (Baseβπ
)) |
26 | | simpllr 774 |
. . . . . . . . . 10
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π β β© πΆ) |
27 | | simpr 485 |
. . . . . . . . . 10
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π β πΆ) |
28 | | elinti 4914 |
. . . . . . . . . . 11
β’ (π β β© πΆ
β (π β πΆ β π β π)) |
29 | 28 | imp 407 |
. . . . . . . . . 10
β’ ((π β β© πΆ
β§ π β πΆ) β π β π) |
30 | 26, 27, 29 | syl2anc 584 |
. . . . . . . . 9
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π β π) |
31 | | eqid 2736 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
32 | 4, 3, 31 | lidlmcl 20672 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (π₯ β (Baseβπ
) β§ π β π)) β (π₯(.rβπ
)π) β π) |
33 | 23, 24, 25, 30, 32 | syl22anc 837 |
. . . . . . . 8
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β (π₯(.rβπ
)π) β π) |
34 | | elinti 4914 |
. . . . . . . . . 10
β’ (π β β© πΆ
β (π β πΆ β π β π)) |
35 | 34 | imp 407 |
. . . . . . . . 9
β’ ((π β β© πΆ
β§ π β πΆ) β π β π) |
36 | 35 | adantll 712 |
. . . . . . . 8
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β π β π) |
37 | | eqid 2736 |
. . . . . . . . 9
β’
(+gβπ
) = (+gβπ
) |
38 | 4, 37 | lidlacl 20668 |
. . . . . . . 8
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ ((π₯(.rβπ
)π) β π β§ π β π)) β ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
39 | 23, 24, 33, 36, 38 | syl22anc 837 |
. . . . . . 7
β’
((((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β§ π β πΆ) β ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
40 | 39 | ralrimiva 3141 |
. . . . . 6
β’
(((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β βπ β πΆ ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
41 | | ovex 7386 |
. . . . . . 7
β’ ((π₯(.rβπ
)π)(+gβπ
)π) β V |
42 | 41 | elint2 4912 |
. . . . . 6
β’ (((π₯(.rβπ
)π)(+gβπ
)π) β β© πΆ β βπ β πΆ ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
43 | 40, 42 | sylibr 233 |
. . . . 5
β’
(((((π
β Ring
β§ πΆ β β
β§
πΆ β
(LIdealβπ
)) β§
π₯ β (Baseβπ
)) β§ π β β© πΆ) β§ π β β© πΆ) β ((π₯(.rβπ
)π)(+gβπ
)π) β β© πΆ) |
44 | 43 | ralrimiva 3141 |
. . . 4
β’ ((((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β§ π₯ β (Baseβπ
)) β§ π β β© πΆ) β βπ β β© πΆ((π₯(.rβπ
)π)(+gβπ
)π) β β© πΆ) |
45 | 44 | anasss 467 |
. . 3
β’ (((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β§ (π₯ β (Baseβπ
) β§ π β β© πΆ)) β βπ β β© πΆ((π₯(.rβπ
)π)(+gβπ
)π) β β© πΆ) |
46 | 45 | ralrimivva 3195 |
. 2
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β βπ₯ β (Baseβπ
)βπ β β© πΆβπ β β© πΆ((π₯(.rβπ
)π)(+gβπ
)π) β β© πΆ) |
47 | 4, 3, 37, 31 | islidl 20666 |
. 2
β’ (β© πΆ
β (LIdealβπ
)
β (β© πΆ β (Baseβπ
) β§ β© πΆ β β
β§
βπ₯ β
(Baseβπ
)βπ β β© πΆβπ β β© πΆ((π₯(.rβπ
)π)(+gβπ
)π) β β© πΆ)) |
48 | 13, 22, 46, 47 | syl3anbrc 1343 |
1
β’ ((π
β Ring β§ πΆ β β
β§ πΆ β (LIdealβπ
)) β β© πΆ
β (LIdealβπ
)) |