Step | Hyp | Ref
| Expression |
1 | | f1oi 6868 |
. . . 4
β’ ( I
βΎ (π RingHom π)):(π RingHom π)β1-1-ontoβ(π RingHom π) |
2 | | f1of 6830 |
. . . 4
β’ (( I
βΎ (π RingHom π)):(π RingHom π)β1-1-ontoβ(π RingHom π) β ( I βΎ (π RingHom π)):(π RingHom π)βΆ(π RingHom π)) |
3 | 1, 2 | mp1i 13 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β ( I βΎ (π RingHom π)):(π RingHom π)βΆ(π RingHom π)) |
4 | | eqid 2732 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
5 | | eqid 2732 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
6 | 4, 5 | rhmf 20255 |
. . . . 5
β’ (π β (π RingHom π) β π:(Baseβπ)βΆ(Baseβπ)) |
7 | | fvex 6901 |
. . . . . . . . . 10
β’
(Baseβπ)
β V |
8 | | fvex 6901 |
. . . . . . . . . 10
β’
(Baseβπ)
β V |
9 | 7, 8 | pm3.2i 471 |
. . . . . . . . 9
β’
((Baseβπ)
β V β§ (Baseβπ) β V) |
10 | | elmapg 8829 |
. . . . . . . . . 10
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (π β ((Baseβπ) βm (Baseβπ)) β π:(Baseβπ)βΆ(Baseβπ))) |
11 | 10 | bicomd 222 |
. . . . . . . . 9
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (π:(Baseβπ)βΆ(Baseβπ) β π β ((Baseβπ) βm (Baseβπ)))) |
12 | 9, 11 | mp1i 13 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π:(Baseβπ)βΆ(Baseβπ) β π β ((Baseβπ) βm (Baseβπ)))) |
13 | 12 | biimpa 477 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π:(Baseβπ)βΆ(Baseβπ)) β π β ((Baseβπ) βm (Baseβπ))) |
14 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β π΅ β§ π β π΅) β π β π΅) |
15 | | funcringcsetcALTV.r |
. . . . . . . . . . 11
β’ π
= (RingCatALTVβπ) |
16 | | funcringcsetcALTV.s |
. . . . . . . . . . 11
β’ π = (SetCatβπ) |
17 | | funcringcsetcALTV.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ
) |
18 | | funcringcsetcALTV.c |
. . . . . . . . . . 11
β’ πΆ = (Baseβπ) |
19 | | funcringcsetcALTV.u |
. . . . . . . . . . 11
β’ (π β π β WUni) |
20 | | funcringcsetcALTV.f |
. . . . . . . . . . 11
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
21 | 15, 16, 17, 18, 19, 20 | funcringcsetclem1ALTV 46910 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
22 | 14, 21 | sylan2 593 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) = (Baseβπ)) |
23 | | simpl 483 |
. . . . . . . . . 10
β’ ((π β π΅ β§ π β π΅) β π β π΅) |
24 | 15, 16, 17, 18, 19, 20 | funcringcsetclem1ALTV 46910 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
25 | 23, 24 | sylan2 593 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) = (Baseβπ)) |
26 | 22, 25 | oveq12d 7423 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((πΉβπ) βm (πΉβπ)) = ((Baseβπ) βm (Baseβπ))) |
27 | 26 | adantr 481 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π:(Baseβπ)βΆ(Baseβπ)) β ((πΉβπ) βm (πΉβπ)) = ((Baseβπ) βm (Baseβπ))) |
28 | 13, 27 | eleqtrrd 2836 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π:(Baseβπ)βΆ(Baseβπ)) β π β ((πΉβπ) βm (πΉβπ))) |
29 | 28 | ex 413 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π:(Baseβπ)βΆ(Baseβπ) β π β ((πΉβπ) βm (πΉβπ)))) |
30 | 6, 29 | syl5 34 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β (π RingHom π) β π β ((πΉβπ) βm (πΉβπ)))) |
31 | 30 | ssrdv 3987 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π RingHom π) β ((πΉβπ) βm (πΉβπ))) |
32 | 3, 31 | fssd 6732 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β ( I βΎ (π RingHom π)):(π RingHom π)βΆ((πΉβπ) βm (πΉβπ))) |
33 | | funcringcsetcALTV.g |
. . . 4
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) |
34 | 15, 16, 17, 18, 19, 20, 33 | funcringcsetclem5ALTV 46914 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) |
35 | 19 | adantr 481 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β WUni) |
36 | | eqid 2732 |
. . . 4
β’ (Hom
βπ
) = (Hom
βπ
) |
37 | 23 | adantl 482 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
38 | 14 | adantl 482 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
39 | 15, 17, 35, 36, 37, 38 | ringchomALTV 46899 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Hom βπ
)π) = (π RingHom π)) |
40 | | eqid 2732 |
. . . 4
β’ (Hom
βπ) = (Hom
βπ) |
41 | 15, 16, 17, 18, 19, 20 | funcringcsetclem2ALTV 46911 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉβπ) β π) |
42 | 23, 41 | sylan2 593 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) β π) |
43 | 15, 16, 17, 18, 19, 20 | funcringcsetclem2ALTV 46911 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉβπ) β π) |
44 | 14, 43 | sylan2 593 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) β π) |
45 | 16, 35, 40, 42, 44 | setchom 18026 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((πΉβπ)(Hom βπ)(πΉβπ)) = ((πΉβπ) βm (πΉβπ))) |
46 | 34, 39, 45 | feq123d 6703 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((ππΊπ):(π(Hom βπ
)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ)) β ( I βΎ (π RingHom π)):(π RingHom π)βΆ((πΉβπ) βm (πΉβπ)))) |
47 | 32, 46 | mpbird 256 |
1
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ
)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) |