Step | Hyp | Ref
| Expression |
1 | | neeq1 3003 |
. . . 4
β’ (π = βͺ
π β (π β π΅ β βͺ π β π΅)) |
2 | | sseq2 3974 |
. . . 4
β’ (π = βͺ
π β (πΌ β π β πΌ β βͺ π)) |
3 | 1, 2 | anbi12d 632 |
. . 3
β’ (π = βͺ
π β ((π β π΅ β§ πΌ β π) β (βͺ π β π΅ β§ πΌ β βͺ π))) |
4 | | ssmxidllem2.1 |
. . . . . . . . 9
β’ (π β π β π) |
5 | | ssmxidllem.1 |
. . . . . . . . . 10
β’ π = {π β (LIdealβπ
) β£ (π β π΅ β§ πΌ β π)} |
6 | 5 | ssrab3 4044 |
. . . . . . . . 9
β’ π β (LIdealβπ
) |
7 | 4, 6 | sstrdi 3960 |
. . . . . . . 8
β’ (π β π β (LIdealβπ
)) |
8 | 7 | sselda 3948 |
. . . . . . 7
β’ ((π β§ π β π) β π β (LIdealβπ
)) |
9 | | ssmxidl.1 |
. . . . . . . 8
β’ π΅ = (Baseβπ
) |
10 | | eqid 2733 |
. . . . . . . 8
β’
(LIdealβπ
) =
(LIdealβπ
) |
11 | 9, 10 | lidlss 20725 |
. . . . . . 7
β’ (π β (LIdealβπ
) β π β π΅) |
12 | 8, 11 | syl 17 |
. . . . . 6
β’ ((π β§ π β π) β π β π΅) |
13 | 12 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π π β π΅) |
14 | | unissb 4904 |
. . . . 5
β’ (βͺ π
β π΅ β
βπ β π π β π΅) |
15 | 13, 14 | sylibr 233 |
. . . 4
β’ (π β βͺ π
β π΅) |
16 | | ssmxidllem2.2 |
. . . . . . 7
β’ (π β π β β
) |
17 | | ssmxidllem.2 |
. . . . . . . . . . 11
β’ (π β π
β Ring) |
18 | 17 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π
β Ring) |
19 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ
) = (0gβπ
) |
20 | 10, 19 | lidl0cl 20727 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π β (LIdealβπ
)) β
(0gβπ
)
β π) |
21 | 18, 8, 20 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π) β (0gβπ
) β π) |
22 | | n0i 4297 |
. . . . . . . . 9
β’
((0gβπ
) β π β Β¬ π = β
) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β Β¬ π = β
) |
24 | 23 | reximdva0 4315 |
. . . . . . 7
β’ ((π β§ π β β
) β βπ β π Β¬ π = β
) |
25 | 16, 24 | mpdan 686 |
. . . . . 6
β’ (π β βπ β π Β¬ π = β
) |
26 | | rexnal 3100 |
. . . . . 6
β’
(βπ β
π Β¬ π = β
β Β¬ βπ β π π = β
) |
27 | 25, 26 | sylib 217 |
. . . . 5
β’ (π β Β¬ βπ β π π = β
) |
28 | | uni0c 4899 |
. . . . . 6
β’ (βͺ π =
β
β βπ
β π π = β
) |
29 | 28 | necon3abii 2987 |
. . . . 5
β’ (βͺ π
β β
β Β¬ βπ β π π = β
) |
30 | 27, 29 | sylibr 233 |
. . . 4
β’ (π β βͺ π
β β
) |
31 | | eluni2 4873 |
. . . . . . . 8
β’ (π β βͺ π
β βπ β
π π β π) |
32 | | eluni2 4873 |
. . . . . . . 8
β’ (π β βͺ π
β βπ β
π π β π) |
33 | 31, 32 | anbi12i 628 |
. . . . . . 7
β’ ((π β βͺ π
β§ π β βͺ π)
β (βπ β
π π β π β§ βπ β π π β π)) |
34 | | an32 645 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π΅) β§ βπ β π π β π) β§ π β π) β (((π β§ π₯ β π΅) β§ π β π) β§ βπ β π π β π)) |
35 | 17 | ad6antr 735 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π
β Ring) |
36 | 7 | ad5antr 733 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β (LIdealβπ
)) |
37 | | simp-4r 783 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
38 | 36, 37 | sseldd 3949 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β (LIdealβπ
)) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β (LIdealβπ
)) |
40 | | simp-6r 787 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π₯ β π΅) |
41 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
42 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
43 | 41, 42 | sseldd 3949 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
44 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(.rβπ
) = (.rβπ
) |
45 | 10, 9, 44 | lidlmcl 20732 |
. . . . . . . . . . . . . . . 16
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (π₯ β π΅ β§ π β π)) β (π₯(.rβπ
)π) β π) |
46 | 35, 39, 40, 43, 45 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β (π₯(.rβπ
)π) β π) |
47 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
48 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(+gβπ
) = (+gβπ
) |
49 | 10, 48 | lidlacl 20728 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ ((π₯(.rβπ
)π) β π β§ π β π)) β ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
50 | 35, 39, 46, 47, 49 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
51 | 37 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
52 | | elunii 4874 |
. . . . . . . . . . . . . 14
β’ ((((π₯(.rβπ
)π)(+gβπ
)π) β π β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
53 | 50, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
54 | 17 | ad6antr 735 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π
β Ring) |
55 | 36 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β (LIdealβπ
)) |
56 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
58 | 55, 57 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β (LIdealβπ
)) |
59 | | simp-6r 787 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π₯ β π΅) |
60 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
61 | 10, 9, 44 | lidlmcl 20732 |
. . . . . . . . . . . . . . . 16
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (π₯ β π΅ β§ π β π)) β (π₯(.rβπ
)π) β π) |
62 | 54, 58, 59, 60, 61 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β (π₯(.rβπ
)π) β π) |
63 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
64 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
65 | 63, 64 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β π β π) |
66 | 10, 48 | lidlacl 20728 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ ((π₯(.rβπ
)π) β π β§ π β π)) β ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
67 | 54, 58, 62, 65, 66 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β π) |
68 | | elunii 4874 |
. . . . . . . . . . . . . 14
β’ ((((π₯(.rβπ
)π)(+gβπ
)π) β π β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
69 | 67, 57, 68 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
70 | | ssmxidllem2.3 |
. . . . . . . . . . . . . . 15
β’ (π β [β] Or π) |
71 | 70 | ad5antr 733 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β [β] Or π) |
72 | | sorpssi 7670 |
. . . . . . . . . . . . . 14
β’ ((
[β] Or π
β§ (π β π β§ π β π)) β (π β π β¨ π β π)) |
73 | 71, 56, 37, 72 | syl12anc 836 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β (π β π β¨ π β π)) |
74 | 53, 69, 73 | mpjaodan 958 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
75 | 74 | r19.29an 3152 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π΅) β§ π β π) β§ π β π) β§ βπ β π π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
76 | 75 | an32s 651 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π΅) β§ π β π) β§ βπ β π π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
77 | 34, 76 | sylanb 582 |
. . . . . . . . 9
β’
(((((π β§ π₯ β π΅) β§ βπ β π π β π) β§ π β π) β§ π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
78 | 77 | r19.29an 3152 |
. . . . . . . 8
β’ ((((π β§ π₯ β π΅) β§ βπ β π π β π) β§ βπ β π π β π) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
79 | 78 | anasss 468 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (βπ β π π β π β§ βπ β π π β π)) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
80 | 33, 79 | sylan2b 595 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π β βͺ π β§ π β βͺ π)) β ((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
81 | 80 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ π₯ β π΅) β βπ β βͺ πβπ β βͺ π((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
82 | 81 | ralrimiva 3140 |
. . . 4
β’ (π β βπ₯ β π΅ βπ β βͺ πβπ β βͺ π((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π) |
83 | 10, 9, 48, 44 | islidl 20726 |
. . . 4
β’ (βͺ π
β (LIdealβπ
)
β (βͺ π β π΅ β§ βͺ π β β
β§
βπ₯ β π΅ βπ β βͺ πβπ β βͺ π((π₯(.rβπ
)π)(+gβπ
)π) β βͺ π)) |
84 | 15, 30, 82, 83 | syl3anbrc 1344 |
. . 3
β’ (π β βͺ π
β (LIdealβπ
)) |
85 | 4 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
86 | | neeq1 3003 |
. . . . . . . . . . . 12
β’ (π = π β (π β π΅ β π β π΅)) |
87 | | sseq2 3974 |
. . . . . . . . . . . 12
β’ (π = π β (πΌ β π β πΌ β π)) |
88 | 86, 87 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = π β ((π β π΅ β§ πΌ β π) β (π β π΅ β§ πΌ β π))) |
89 | 88, 5 | elrab2 3652 |
. . . . . . . . . 10
β’ (π β π β (π β (LIdealβπ
) β§ (π β π΅ β§ πΌ β π))) |
90 | 85, 89 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π β (LIdealβπ
) β§ (π β π΅ β§ πΌ β π))) |
91 | 90 | simprld 771 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π΅) |
92 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ
) = (1rβπ
) |
93 | 9, 92 | pridln1 32270 |
. . . . . . . 8
β’ ((π
β Ring β§ π β (LIdealβπ
) β§ π β π΅) β Β¬ (1rβπ
) β π) |
94 | 18, 8, 91, 93 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β π) β Β¬ (1rβπ
) β π) |
95 | 94 | nrexdv 3143 |
. . . . . 6
β’ (π β Β¬ βπ β π (1rβπ
) β π) |
96 | | eluni2 4873 |
. . . . . 6
β’
((1rβπ
) β βͺ π β βπ β π (1rβπ
) β π) |
97 | 95, 96 | sylnibr 329 |
. . . . 5
β’ (π β Β¬
(1rβπ
)
β βͺ π) |
98 | 10, 9, 92 | lidl1el 20733 |
. . . . . . 7
β’ ((π
β Ring β§ βͺ π
β (LIdealβπ
))
β ((1rβπ
) β βͺ π β βͺ π =
π΅)) |
99 | 17, 84, 98 | syl2anc 585 |
. . . . . 6
β’ (π β
((1rβπ
)
β βͺ π β βͺ π = π΅)) |
100 | 99 | necon3bbid 2978 |
. . . . 5
β’ (π β (Β¬
(1rβπ
)
β βͺ π β βͺ π β π΅)) |
101 | 97, 100 | mpbid 231 |
. . . 4
β’ (π β βͺ π
β π΅) |
102 | 90 | simprrd 773 |
. . . . . . 7
β’ ((π β§ π β π) β πΌ β π) |
103 | 102 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ β π πΌ β π) |
104 | | ssint 4929 |
. . . . . 6
β’ (πΌ β β© π
β βπ β
π πΌ β π) |
105 | 103, 104 | sylibr 233 |
. . . . 5
β’ (π β πΌ β β© π) |
106 | | intssuni 4935 |
. . . . . 6
β’ (π β β
β β© π
β βͺ π) |
107 | 16, 106 | syl 17 |
. . . . 5
β’ (π β β© π
β βͺ π) |
108 | 105, 107 | sstrd 3958 |
. . . 4
β’ (π β πΌ β βͺ π) |
109 | 101, 108 | jca 513 |
. . 3
β’ (π β (βͺ π
β π΅ β§ πΌ β βͺ π)) |
110 | 3, 84, 109 | elrabd 3651 |
. 2
β’ (π β βͺ π
β {π β
(LIdealβπ
) β£
(π β π΅ β§ πΌ β π)}) |
111 | 110, 5 | eleqtrrdi 2845 |
1
β’ (π β βͺ π
β π) |