Step | Hyp | Ref
| Expression |
1 | | rnghmsubcsetc.b |
. . . . . 6
β’ (π β π΅ = (Rng β© π)) |
2 | 1 | eleq2d 2818 |
. . . . 5
β’ (π β (π₯ β π΅ β π₯ β (Rng β© π))) |
3 | | elin 3944 |
. . . . . 6
β’ (π₯ β (Rng β© π) β (π₯ β Rng β§ π₯ β π)) |
4 | 3 | simplbi 498 |
. . . . 5
β’ (π₯ β (Rng β© π) β π₯ β Rng) |
5 | 2, 4 | syl6bi 252 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β Rng)) |
6 | 5 | imp 407 |
. . 3
β’ ((π β§ π₯ β π΅) β π₯ β Rng) |
7 | | eqid 2731 |
. . . 4
β’
(Baseβπ₯) =
(Baseβπ₯) |
8 | 7 | idrnghm 46359 |
. . 3
β’ (π₯ β Rng β ( I βΎ
(Baseβπ₯)) β
(π₯ RngHomo π₯)) |
9 | 6, 8 | syl 17 |
. 2
β’ ((π β§ π₯ β π΅) β ( I βΎ (Baseβπ₯)) β (π₯ RngHomo π₯)) |
10 | | rnghmsubcsetc.c |
. . 3
β’ πΆ = (ExtStrCatβπ) |
11 | | eqid 2731 |
. . 3
β’
(IdβπΆ) =
(IdβπΆ) |
12 | | rnghmsubcsetc.u |
. . . 4
β’ (π β π β π) |
13 | 12 | adantr 481 |
. . 3
β’ ((π β§ π₯ β π΅) β π β π) |
14 | 3 | simprbi 497 |
. . . . 5
β’ (π₯ β (Rng β© π) β π₯ β π) |
15 | 2, 14 | syl6bi 252 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β π)) |
16 | 15 | imp 407 |
. . 3
β’ ((π β§ π₯ β π΅) β π₯ β π) |
17 | 10, 11, 13, 16 | estrcid 18050 |
. 2
β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) = ( I βΎ (Baseβπ₯))) |
18 | | rnghmsubcsetc.h |
. . . 4
β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) |
19 | 18 | oveqdr 7405 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯π»π₯) = (π₯( RngHomo βΎ (π΅ Γ π΅))π₯)) |
20 | | eqid 2731 |
. . . . . . . 8
β’
(RngCatβπ) =
(RngCatβπ) |
21 | | eqid 2731 |
. . . . . . . 8
β’
(Baseβ(RngCatβπ)) = (Baseβ(RngCatβπ)) |
22 | | eqid 2731 |
. . . . . . . 8
β’ (Hom
β(RngCatβπ)) =
(Hom β(RngCatβπ)) |
23 | 20, 21, 12, 22 | rngchomfval 46417 |
. . . . . . 7
β’ (π β (Hom
β(RngCatβπ)) =
( RngHomo βΎ ((Baseβ(RngCatβπ)) Γ (Baseβ(RngCatβπ))))) |
24 | 20, 21, 12 | rngcbas 46416 |
. . . . . . . . . 10
β’ (π β
(Baseβ(RngCatβπ)) = (π β© Rng)) |
25 | | incom 4181 |
. . . . . . . . . . . 12
β’ (Rng
β© π) = (π β© Rng) |
26 | 1, 25 | eqtrdi 2787 |
. . . . . . . . . . 11
β’ (π β π΅ = (π β© Rng)) |
27 | 26 | eqcomd 2737 |
. . . . . . . . . 10
β’ (π β (π β© Rng) = π΅) |
28 | 24, 27 | eqtrd 2771 |
. . . . . . . . 9
β’ (π β
(Baseβ(RngCatβπ)) = π΅) |
29 | 28 | sqxpeqd 5685 |
. . . . . . . 8
β’ (π β
((Baseβ(RngCatβπ)) Γ (Baseβ(RngCatβπ))) = (π΅ Γ π΅)) |
30 | 29 | reseq2d 5957 |
. . . . . . 7
β’ (π β ( RngHomo βΎ
((Baseβ(RngCatβπ)) Γ (Baseβ(RngCatβπ)))) = ( RngHomo βΎ (π΅ Γ π΅))) |
31 | 23, 30 | eqtrd 2771 |
. . . . . 6
β’ (π β (Hom
β(RngCatβπ)) =
( RngHomo βΎ (π΅
Γ π΅))) |
32 | 31 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (Hom β(RngCatβπ)) = ( RngHomo βΎ (π΅ Γ π΅))) |
33 | 32 | eqcomd 2737 |
. . . 4
β’ ((π β§ π₯ β π΅) β ( RngHomo βΎ (π΅ Γ π΅)) = (Hom β(RngCatβπ))) |
34 | 33 | oveqd 7394 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯( RngHomo βΎ (π΅ Γ π΅))π₯) = (π₯(Hom β(RngCatβπ))π₯)) |
35 | 26 | eleq2d 2818 |
. . . . . 6
β’ (π β (π₯ β π΅ β π₯ β (π β© Rng))) |
36 | 35 | biimpa 477 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π₯ β (π β© Rng)) |
37 | 24 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (Baseβ(RngCatβπ)) = (π β© Rng)) |
38 | 36, 37 | eleqtrrd 2835 |
. . . 4
β’ ((π β§ π₯ β π΅) β π₯ β (Baseβ(RngCatβπ))) |
39 | 20, 21, 13, 22, 38, 38 | rngchom 46418 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯(Hom β(RngCatβπ))π₯) = (π₯ RngHomo π₯)) |
40 | 19, 34, 39 | 3eqtrd 2775 |
. 2
β’ ((π β§ π₯ β π΅) β (π₯π»π₯) = (π₯ RngHomo π₯)) |
41 | 9, 17, 40 | 3eltr4d 2847 |
1
β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) |