Step | Hyp | Ref
| Expression |
1 | | rngcrescrhmALTV.r |
. . . . . 6
β’ (π β π
= (Ring β© π)) |
2 | 1 | eleq2d 2820 |
. . . . 5
β’ (π β (π₯ β π
β π₯ β (Ring β© π))) |
3 | | elinel1 4159 |
. . . . 5
β’ (π₯ β (Ring β© π) β π₯ β Ring) |
4 | 2, 3 | syl6bi 253 |
. . . 4
β’ (π β (π₯ β π
β π₯ β Ring)) |
5 | 4 | imp 408 |
. . 3
β’ ((π β§ π₯ β π
) β π₯ β Ring) |
6 | | eqid 2733 |
. . . 4
β’
(Baseβπ₯) =
(Baseβπ₯) |
7 | 6 | idrhm 20173 |
. . 3
β’ (π₯ β Ring β ( I βΎ
(Baseβπ₯)) β
(π₯ RingHom π₯)) |
8 | 5, 7 | syl 17 |
. 2
β’ ((π β§ π₯ β π
) β ( I βΎ (Baseβπ₯)) β (π₯ RingHom π₯)) |
9 | | rngcrescrhmALTV.u |
. . . . 5
β’ (π β π β π) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π
) β π β π) |
11 | | eqid 2733 |
. . . . 5
β’
(RngCatALTVβπ)
= (RngCatALTVβπ) |
12 | | eqid 2733 |
. . . . 5
β’
(Baseβ(RngCatALTVβπ)) = (Baseβ(RngCatALTVβπ)) |
13 | 11, 12 | rngccatidALTV 46377 |
. . . 4
β’ (π β π β ((RngCatALTVβπ) β Cat β§
(Idβ(RngCatALTVβπ)) = (π¦ β (Baseβ(RngCatALTVβπ)) β¦ ( I βΎ
(Baseβπ¦))))) |
14 | | simpr 486 |
. . . 4
β’
(((RngCatALTVβπ) β Cat β§
(Idβ(RngCatALTVβπ)) = (π¦ β (Baseβ(RngCatALTVβπ)) β¦ ( I βΎ
(Baseβπ¦)))) β
(Idβ(RngCatALTVβπ)) = (π¦ β (Baseβ(RngCatALTVβπ)) β¦ ( I βΎ
(Baseβπ¦)))) |
15 | 10, 13, 14 | 3syl 18 |
. . 3
β’ ((π β§ π₯ β π
) β (Idβ(RngCatALTVβπ)) = (π¦ β (Baseβ(RngCatALTVβπ)) β¦ ( I βΎ
(Baseβπ¦)))) |
16 | | fveq2 6846 |
. . . . 5
β’ (π¦ = π₯ β (Baseβπ¦) = (Baseβπ₯)) |
17 | 16 | reseq2d 5941 |
. . . 4
β’ (π¦ = π₯ β ( I βΎ (Baseβπ¦)) = ( I βΎ
(Baseβπ₯))) |
18 | 17 | adantl 483 |
. . 3
β’ (((π β§ π₯ β π
) β§ π¦ = π₯) β ( I βΎ (Baseβπ¦)) = ( I βΎ
(Baseβπ₯))) |
19 | | incom 4165 |
. . . . . . . 8
β’ (Ring
β© π) = (π β© Ring) |
20 | 1, 19 | eqtrdi 2789 |
. . . . . . 7
β’ (π β π
= (π β© Ring)) |
21 | 20 | eleq2d 2820 |
. . . . . 6
β’ (π β (π₯ β π
β π₯ β (π β© Ring))) |
22 | | ringrng 46267 |
. . . . . . . 8
β’ (π₯ β Ring β π₯ β Rng) |
23 | 22 | anim2i 618 |
. . . . . . 7
β’ ((π₯ β π β§ π₯ β Ring) β (π₯ β π β§ π₯ β Rng)) |
24 | | elin 3930 |
. . . . . . 7
β’ (π₯ β (π β© Ring) β (π₯ β π β§ π₯ β Ring)) |
25 | | elin 3930 |
. . . . . . 7
β’ (π₯ β (π β© Rng) β (π₯ β π β§ π₯ β Rng)) |
26 | 23, 24, 25 | 3imtr4i 292 |
. . . . . 6
β’ (π₯ β (π β© Ring) β π₯ β (π β© Rng)) |
27 | 21, 26 | syl6bi 253 |
. . . . 5
β’ (π β (π₯ β π
β π₯ β (π β© Rng))) |
28 | 27 | imp 408 |
. . . 4
β’ ((π β§ π₯ β π
) β π₯ β (π β© Rng)) |
29 | | rngcrescrhmALTV.c |
. . . . . 6
β’ πΆ = (RngCatALTVβπ) |
30 | 29 | eqcomi 2742 |
. . . . . . 7
β’
(RngCatALTVβπ)
= πΆ |
31 | 30 | fveq2i 6849 |
. . . . . 6
β’
(Baseβ(RngCatALTVβπ)) = (BaseβπΆ) |
32 | 29, 31, 9 | rngcbasALTV 46371 |
. . . . 5
β’ (π β
(Baseβ(RngCatALTVβπ)) = (π β© Rng)) |
33 | 32 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π
) β (Baseβ(RngCatALTVβπ)) = (π β© Rng)) |
34 | 28, 33 | eleqtrrd 2837 |
. . 3
β’ ((π β§ π₯ β π
) β π₯ β (Baseβ(RngCatALTVβπ))) |
35 | | fvexd 6861 |
. . . 4
β’ ((π β§ π₯ β π
) β (Baseβπ₯) β V) |
36 | 35 | resiexd 7170 |
. . 3
β’ ((π β§ π₯ β π
) β ( I βΎ (Baseβπ₯)) β V) |
37 | 15, 18, 34, 36 | fvmptd 6959 |
. 2
β’ ((π β§ π₯ β π
) β ((Idβ(RngCatALTVβπ))βπ₯) = ( I βΎ (Baseβπ₯))) |
38 | | rngcrescrhmALTV.h |
. . . 4
β’ π» = ( RingHom βΎ (π
Γ π
)) |
39 | 9, 29, 1, 38 | rhmsubcALTVlem2 46493 |
. . 3
β’ ((π β§ π₯ β π
β§ π₯ β π
) β (π₯π»π₯) = (π₯ RingHom π₯)) |
40 | 39 | 3anidm23 1422 |
. 2
β’ ((π β§ π₯ β π
) β (π₯π»π₯) = (π₯ RingHom π₯)) |
41 | 8, 37, 40 | 3eltr4d 2849 |
1
β’ ((π β§ π₯ β π
) β ((Idβ(RngCatALTVβπ))βπ₯) β (π₯π»π₯)) |