Step | Hyp | Ref
| Expression |
1 | | evlseu.p |
. . . 4
β’ π = (πΌ mPoly π
) |
2 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
3 | | evlseu.c |
. . . 4
β’ πΆ = (Baseβπ) |
4 | | eqid 2733 |
. . . 4
β’ {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} = {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β
Fin} |
5 | | eqid 2733 |
. . . 4
β’
(mulGrpβπ) =
(mulGrpβπ) |
6 | | eqid 2733 |
. . . 4
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
7 | | eqid 2733 |
. . . 4
β’
(.rβπ) = (.rβπ) |
8 | | evlseu.v |
. . . 4
β’ π = (πΌ mVar π
) |
9 | | eqid 2733 |
. . . 4
β’ (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) = (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) |
10 | | evlseu.i |
. . . 4
β’ (π β πΌ β π) |
11 | | evlseu.r |
. . . 4
β’ (π β π
β CRing) |
12 | | evlseu.s |
. . . 4
β’ (π β π β CRing) |
13 | | evlseu.f |
. . . 4
β’ (π β πΉ β (π
RingHom π)) |
14 | | evlseu.g |
. . . 4
β’ (π β πΊ:πΌβΆπΆ) |
15 | | evlseu.a |
. . . 4
β’ π΄ = (algScβπ) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | evlslem1 21645 |
. . 3
β’ (π β ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β (π RingHom π) β§ ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π΄) = πΉ β§ ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π) = πΊ)) |
17 | | coeq1 5858 |
. . . . . . 7
β’ (π = (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β (π β π΄) = ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π΄)) |
18 | 17 | eqeq1d 2735 |
. . . . . 6
β’ (π = (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β ((π β π΄) = πΉ β ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π΄) = πΉ)) |
19 | | coeq1 5858 |
. . . . . . 7
β’ (π = (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β (π β π) = ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π)) |
20 | 19 | eqeq1d 2735 |
. . . . . 6
β’ (π = (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β ((π β π) = πΊ β ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π) = πΊ)) |
21 | 18, 20 | anbi12d 632 |
. . . . 5
β’ (π = (π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β (((π β π΄) = πΉ β§ (π β π) = πΊ) β (((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π΄) = πΉ β§ ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π) = πΊ))) |
22 | 21 | rspcev 3613 |
. . . 4
β’ (((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β (π RingHom π) β§ (((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π΄) = πΉ β§ ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π) = πΊ)) β βπ β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) |
23 | 22 | 3impb 1116 |
. . 3
β’ (((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β (π RingHom π) β§ ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π΄) = πΉ β§ ((π₯ β (Baseβπ) β¦ (π Ξ£g (π¦ β {π§ β (β0
βm πΌ)
β£ (β‘π§ β β) β Fin} β¦ ((πΉβ(π₯βπ¦))(.rβπ)((mulGrpβπ) Ξ£g (π¦ βf
(.gβ(mulGrpβπ))πΊ)))))) β π) = πΊ) β βπ β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) |
24 | 16, 23 | syl 17 |
. 2
β’ (π β βπ β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) |
25 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
26 | | crngring 20068 |
. . . . . . . . . . 11
β’ (π
β CRing β π
β Ring) |
27 | 11, 26 | syl 17 |
. . . . . . . . . 10
β’ (π β π
β Ring) |
28 | 1, 2, 25, 15, 10, 27 | mplasclf 21626 |
. . . . . . . . 9
β’ (π β π΄:(Baseβπ
)βΆ(Baseβπ)) |
29 | 28 | ffund 6722 |
. . . . . . . 8
β’ (π β Fun π΄) |
30 | | funcoeqres 6865 |
. . . . . . . 8
β’ ((Fun
π΄ β§ (π β π΄) = πΉ) β (π βΎ ran π΄) = (πΉ β β‘π΄)) |
31 | 29, 30 | sylan 581 |
. . . . . . 7
β’ ((π β§ (π β π΄) = πΉ) β (π βΎ ran π΄) = (πΉ β β‘π΄)) |
32 | 1, 8, 2, 10, 27 | mvrf2 21552 |
. . . . . . . . 9
β’ (π β π:πΌβΆ(Baseβπ)) |
33 | 32 | ffund 6722 |
. . . . . . . 8
β’ (π β Fun π) |
34 | | funcoeqres 6865 |
. . . . . . . 8
β’ ((Fun
π β§ (π β π) = πΊ) β (π βΎ ran π) = (πΊ β β‘π)) |
35 | 33, 34 | sylan 581 |
. . . . . . 7
β’ ((π β§ (π β π) = πΊ) β (π βΎ ran π) = (πΊ β β‘π)) |
36 | 31, 35 | anim12dan 620 |
. . . . . 6
β’ ((π β§ ((π β π΄) = πΉ β§ (π β π) = πΊ)) β ((π βΎ ran π΄) = (πΉ β β‘π΄) β§ (π βΎ ran π) = (πΊ β β‘π))) |
37 | 36 | ex 414 |
. . . . 5
β’ (π β (((π β π΄) = πΉ β§ (π β π) = πΊ) β ((π βΎ ran π΄) = (πΉ β β‘π΄) β§ (π βΎ ran π) = (πΊ β β‘π)))) |
38 | | resundi 5996 |
. . . . . 6
β’ (π βΎ (ran π΄ βͺ ran π)) = ((π βΎ ran π΄) βͺ (π βΎ ran π)) |
39 | | uneq12 4159 |
. . . . . 6
β’ (((π βΎ ran π΄) = (πΉ β β‘π΄) β§ (π βΎ ran π) = (πΊ β β‘π)) β ((π βΎ ran π΄) βͺ (π βΎ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) |
40 | 38, 39 | eqtrid 2785 |
. . . . 5
β’ (((π βΎ ran π΄) = (πΉ β β‘π΄) β§ (π βΎ ran π) = (πΊ β β‘π)) β (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) |
41 | 37, 40 | syl6 35 |
. . . 4
β’ (π β (((π β π΄) = πΉ β§ (π β π) = πΊ) β (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)))) |
42 | 41 | ralrimivw 3151 |
. . 3
β’ (π β βπ β (π RingHom π)(((π β π΄) = πΉ β§ (π β π) = πΊ) β (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)))) |
43 | | eqtr3 2759 |
. . . . . 6
β’ (((π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β§ (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) β (π βΎ (ran π΄ βͺ ran π)) = (π βΎ (ran π΄ βͺ ran π))) |
44 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (πΌ mPwSer π
) = (πΌ mPwSer π
) |
45 | 44, 10, 11 | psrassa 21534 |
. . . . . . . . . . . 12
β’ (π β (πΌ mPwSer π
) β AssAlg) |
46 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβ(πΌ
mPwSer π
)) =
(Baseβ(πΌ mPwSer π
)) |
47 | 44, 8, 46, 10, 27 | mvrf 21544 |
. . . . . . . . . . . . 13
β’ (π β π:πΌβΆ(Baseβ(πΌ mPwSer π
))) |
48 | 47 | frnd 6726 |
. . . . . . . . . . . 12
β’ (π β ran π β (Baseβ(πΌ mPwSer π
))) |
49 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(AlgSpanβ(πΌ
mPwSer π
)) =
(AlgSpanβ(πΌ mPwSer
π
)) |
50 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(algScβ(πΌ
mPwSer π
)) =
(algScβ(πΌ mPwSer
π
)) |
51 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(mrClsβ(SubRingβ(πΌ mPwSer π
))) = (mrClsβ(SubRingβ(πΌ mPwSer π
))) |
52 | 49, 50, 51, 46 | aspval2 21452 |
. . . . . . . . . . . 12
β’ (((πΌ mPwSer π
) β AssAlg β§ ran π β (Baseβ(πΌ mPwSer π
))) β ((AlgSpanβ(πΌ mPwSer π
))βran π) = ((mrClsβ(SubRingβ(πΌ mPwSer π
)))β(ran (algScβ(πΌ mPwSer π
)) βͺ ran π))) |
53 | 45, 48, 52 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((AlgSpanβ(πΌ mPwSer π
))βran π) = ((mrClsβ(SubRingβ(πΌ mPwSer π
)))β(ran (algScβ(πΌ mPwSer π
)) βͺ ran π))) |
54 | 1, 44, 8, 49, 10, 11 | mplbas2 21597 |
. . . . . . . . . . 11
β’ (π β ((AlgSpanβ(πΌ mPwSer π
))βran π) = (Baseβπ)) |
55 | 44, 1, 2, 10, 27 | mplsubrg 21564 |
. . . . . . . . . . . . . . 15
β’ (π β (Baseβπ) β (SubRingβ(πΌ mPwSer π
))) |
56 | 1, 44, 2 | mplval2 21555 |
. . . . . . . . . . . . . . . 16
β’ π = ((πΌ mPwSer π
) βΎs (Baseβπ)) |
57 | 56 | subsubrg2 20346 |
. . . . . . . . . . . . . . 15
β’
((Baseβπ)
β (SubRingβ(πΌ
mPwSer π
)) β
(SubRingβπ) =
((SubRingβ(πΌ mPwSer
π
)) β© π«
(Baseβπ))) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (SubRingβπ) = ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ))) |
59 | 58 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (π β
(mrClsβ(SubRingβπ)) = (mrClsβ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ)))) |
60 | 50, 56 | ressascl 21450 |
. . . . . . . . . . . . . . . . 17
β’
((Baseβπ)
β (SubRingβ(πΌ
mPwSer π
)) β
(algScβ(πΌ mPwSer
π
)) = (algScβπ)) |
61 | 55, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (algScβ(πΌ mPwSer π
)) = (algScβπ)) |
62 | 15, 61 | eqtr4id 2792 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ = (algScβ(πΌ mPwSer π
))) |
63 | 62 | rneqd 5938 |
. . . . . . . . . . . . . 14
β’ (π β ran π΄ = ran (algScβ(πΌ mPwSer π
))) |
64 | 63 | uneq1d 4163 |
. . . . . . . . . . . . 13
β’ (π β (ran π΄ βͺ ran π) = (ran (algScβ(πΌ mPwSer π
)) βͺ ran π)) |
65 | 59, 64 | fveq12d 6899 |
. . . . . . . . . . . 12
β’ (π β
((mrClsβ(SubRingβπ))β(ran π΄ βͺ ran π)) = ((mrClsβ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ)))β(ran
(algScβ(πΌ mPwSer
π
)) βͺ ran π))) |
66 | | assaring 21416 |
. . . . . . . . . . . . . 14
β’ ((πΌ mPwSer π
) β AssAlg β (πΌ mPwSer π
) β Ring) |
67 | 46 | subrgmre 20344 |
. . . . . . . . . . . . . 14
β’ ((πΌ mPwSer π
) β Ring β (SubRingβ(πΌ mPwSer π
)) β (Mooreβ(Baseβ(πΌ mPwSer π
)))) |
68 | 45, 66, 67 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β (SubRingβ(πΌ mPwSer π
)) β (Mooreβ(Baseβ(πΌ mPwSer π
)))) |
69 | 28 | frnd 6726 |
. . . . . . . . . . . . . . 15
β’ (π β ran π΄ β (Baseβπ)) |
70 | 63, 69 | eqsstrrd 4022 |
. . . . . . . . . . . . . 14
β’ (π β ran (algScβ(πΌ mPwSer π
)) β (Baseβπ)) |
71 | 32 | frnd 6726 |
. . . . . . . . . . . . . 14
β’ (π β ran π β (Baseβπ)) |
72 | 70, 71 | unssd 4187 |
. . . . . . . . . . . . 13
β’ (π β (ran (algScβ(πΌ mPwSer π
)) βͺ ran π) β (Baseβπ)) |
73 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(mrClsβ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ))) =
(mrClsβ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ))) |
74 | 51, 73 | submrc 17572 |
. . . . . . . . . . . . 13
β’
(((SubRingβ(πΌ
mPwSer π
)) β
(Mooreβ(Baseβ(πΌ
mPwSer π
))) β§
(Baseβπ) β
(SubRingβ(πΌ mPwSer
π
)) β§ (ran
(algScβ(πΌ mPwSer
π
)) βͺ ran π) β (Baseβπ)) β
((mrClsβ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ)))β(ran
(algScβ(πΌ mPwSer
π
)) βͺ ran π)) =
((mrClsβ(SubRingβ(πΌ mPwSer π
)))β(ran (algScβ(πΌ mPwSer π
)) βͺ ran π))) |
75 | 68, 55, 72, 74 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β
((mrClsβ((SubRingβ(πΌ mPwSer π
)) β© π« (Baseβπ)))β(ran
(algScβ(πΌ mPwSer
π
)) βͺ ran π)) =
((mrClsβ(SubRingβ(πΌ mPwSer π
)))β(ran (algScβ(πΌ mPwSer π
)) βͺ ran π))) |
76 | 65, 75 | eqtr2d 2774 |
. . . . . . . . . . 11
β’ (π β
((mrClsβ(SubRingβ(πΌ mPwSer π
)))β(ran (algScβ(πΌ mPwSer π
)) βͺ ran π)) = ((mrClsβ(SubRingβπ))β(ran π΄ βͺ ran π))) |
77 | 53, 54, 76 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ (π β (Baseβπ) =
((mrClsβ(SubRingβπ))β(ran π΄ βͺ ran π))) |
78 | 77 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β§ (ran π΄ βͺ ran π) β dom (π β© π)) β (Baseβπ) = ((mrClsβ(SubRingβπ))β(ran π΄ βͺ ran π))) |
79 | 1 | mplring 21578 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
80 | 10, 27, 79 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β π β Ring) |
81 | 2 | subrgmre 20344 |
. . . . . . . . . . . 12
β’ (π β Ring β
(SubRingβπ) β
(Mooreβ(Baseβπ))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
β’ (π β (SubRingβπ) β
(Mooreβ(Baseβπ))) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β§ (ran π΄ βͺ ran π) β dom (π β© π)) β (SubRingβπ) β (Mooreβ(Baseβπ))) |
84 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β§ (ran π΄ βͺ ran π) β dom (π β© π)) β (ran π΄ βͺ ran π) β dom (π β© π)) |
85 | | rhmeql 20350 |
. . . . . . . . . . 11
β’ ((π β (π RingHom π) β§ π β (π RingHom π)) β dom (π β© π) β (SubRingβπ)) |
86 | 85 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β§ (ran π΄ βͺ ran π) β dom (π β© π)) β dom (π β© π) β (SubRingβπ)) |
87 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mrClsβ(SubRingβπ)) = (mrClsβ(SubRingβπ)) |
88 | 87 | mrcsscl 17564 |
. . . . . . . . . 10
β’
(((SubRingβπ)
β (Mooreβ(Baseβπ)) β§ (ran π΄ βͺ ran π) β dom (π β© π) β§ dom (π β© π) β (SubRingβπ)) β ((mrClsβ(SubRingβπ))β(ran π΄ βͺ ran π)) β dom (π β© π)) |
89 | 83, 84, 86, 88 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β§ (ran π΄ βͺ ran π) β dom (π β© π)) β ((mrClsβ(SubRingβπ))β(ran π΄ βͺ ran π)) β dom (π β© π)) |
90 | 78, 89 | eqsstrd 4021 |
. . . . . . . 8
β’ (((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β§ (ran π΄ βͺ ran π) β dom (π β© π)) β (Baseβπ) β dom (π β© π)) |
91 | 90 | ex 414 |
. . . . . . 7
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β ((ran π΄ βͺ ran π) β dom (π β© π) β (Baseβπ) β dom (π β© π))) |
92 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β π β (π RingHom π)) |
93 | 2, 3 | rhmf 20263 |
. . . . . . . . 9
β’ (π β (π RingHom π) β π:(Baseβπ)βΆπΆ) |
94 | | ffn 6718 |
. . . . . . . . 9
β’ (π:(Baseβπ)βΆπΆ β π Fn (Baseβπ)) |
95 | 92, 93, 94 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β π Fn (Baseβπ)) |
96 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β π β (π RingHom π)) |
97 | 2, 3 | rhmf 20263 |
. . . . . . . . 9
β’ (π β (π RingHom π) β π:(Baseβπ)βΆπΆ) |
98 | | ffn 6718 |
. . . . . . . . 9
β’ (π:(Baseβπ)βΆπΆ β π Fn (Baseβπ)) |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β π Fn (Baseβπ)) |
100 | 69 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β ran π΄ β (Baseβπ)) |
101 | 71 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β ran π β (Baseβπ)) |
102 | 100, 101 | unssd 4187 |
. . . . . . . 8
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β (ran π΄ βͺ ran π) β (Baseβπ)) |
103 | | fnreseql 7050 |
. . . . . . . 8
β’ ((π Fn (Baseβπ) β§ π Fn (Baseβπ) β§ (ran π΄ βͺ ran π) β (Baseβπ)) β ((π βΎ (ran π΄ βͺ ran π)) = (π βΎ (ran π΄ βͺ ran π)) β (ran π΄ βͺ ran π) β dom (π β© π))) |
104 | 95, 99, 102, 103 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β ((π βΎ (ran π΄ βͺ ran π)) = (π βΎ (ran π΄ βͺ ran π)) β (ran π΄ βͺ ran π) β dom (π β© π))) |
105 | | fneqeql2 7049 |
. . . . . . . 8
β’ ((π Fn (Baseβπ) β§ π Fn (Baseβπ)) β (π = π β (Baseβπ) β dom (π β© π))) |
106 | 95, 99, 105 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β (π = π β (Baseβπ) β dom (π β© π))) |
107 | 91, 104, 106 | 3imtr4d 294 |
. . . . . 6
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β ((π βΎ (ran π΄ βͺ ran π)) = (π βΎ (ran π΄ βͺ ran π)) β π = π)) |
108 | 43, 107 | syl5 34 |
. . . . 5
β’ ((π β§ (π β (π RingHom π) β§ π β (π RingHom π))) β (((π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β§ (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) β π = π)) |
109 | 108 | ralrimivva 3201 |
. . . 4
β’ (π β βπ β (π RingHom π)βπ β (π RingHom π)(((π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β§ (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) β π = π)) |
110 | | reseq1 5976 |
. . . . . 6
β’ (π = π β (π βΎ (ran π΄ βͺ ran π)) = (π βΎ (ran π΄ βͺ ran π))) |
111 | 110 | eqeq1d 2735 |
. . . . 5
β’ (π = π β ((π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)))) |
112 | 111 | rmo4 3727 |
. . . 4
β’
(β*π β
(π RingHom π)(π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β βπ β (π RingHom π)βπ β (π RingHom π)(((π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β§ (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) β π = π)) |
113 | 109, 112 | sylibr 233 |
. . 3
β’ (π β β*π β (π RingHom π)(π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) |
114 | | rmoim 3737 |
. . 3
β’
(βπ β
(π RingHom π)(((π β π΄) = πΉ β§ (π β π) = πΊ) β (π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π))) β (β*π β (π RingHom π)(π βΎ (ran π΄ βͺ ran π)) = ((πΉ β β‘π΄) βͺ (πΊ β β‘π)) β β*π β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ))) |
115 | 42, 113, 114 | sylc 65 |
. 2
β’ (π β β*π β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) |
116 | | reu5 3379 |
. 2
β’
(β!π β
(π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ) β (βπ β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ) β§ β*π β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ))) |
117 | 24, 115, 116 | sylanbrc 584 |
1
β’ (π β β!π β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) |