Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . . 8
β’ ((π β§ π₯ β π
) β π) |
2 | 1 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π) |
3 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β π
) β π₯ β π
) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π₯ β π
) |
5 | | simpl 484 |
. . . . . . . 8
β’ ((π¦ β π
β§ π§ β π
) β π¦ β π
) |
6 | 5 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π¦ β π
) |
7 | | rngcrescrhmALTV.u |
. . . . . . . 8
β’ (π β π β π) |
8 | | rngcrescrhmALTV.c |
. . . . . . . 8
β’ πΆ = (RngCatALTVβπ) |
9 | | rngcrescrhmALTV.r |
. . . . . . . 8
β’ (π β π
= (Ring β© π)) |
10 | | rngcrescrhmALTV.h |
. . . . . . . 8
β’ π» = ( RingHom βΎ (π
Γ π
)) |
11 | 7, 8, 9, 10 | rhmsubcALTVlem2 46493 |
. . . . . . 7
β’ ((π β§ π₯ β π
β§ π¦ β π
) β (π₯π»π¦) = (π₯ RingHom π¦)) |
12 | 2, 4, 6, 11 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π₯π»π¦) = (π₯ RingHom π¦)) |
13 | 12 | eleq2d 2820 |
. . . . 5
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π₯π»π¦) β π β (π₯ RingHom π¦))) |
14 | | simpr 486 |
. . . . . . . 8
β’ ((π¦ β π
β§ π§ β π
) β π§ β π
) |
15 | 14 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π§ β π
) |
16 | 7, 8, 9, 10 | rhmsubcALTVlem2 46493 |
. . . . . . 7
β’ ((π β§ π¦ β π
β§ π§ β π
) β (π¦π»π§) = (π¦ RingHom π§)) |
17 | 2, 6, 15, 16 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π¦π»π§) = (π¦ RingHom π§)) |
18 | 17 | eleq2d 2820 |
. . . . 5
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π¦π»π§) β π β (π¦ RingHom π§))) |
19 | 13, 18 | anbi12d 632 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (π β (π₯ RingHom π¦) β§ π β (π¦ RingHom π§)))) |
20 | | rhmco 20181 |
. . . . 5
β’ ((π β (π¦ RingHom π§) β§ π β (π₯ RingHom π¦)) β (π β π) β (π₯ RingHom π§)) |
21 | 20 | ancoms 460 |
. . . 4
β’ ((π β (π₯ RingHom π¦) β§ π β (π¦ RingHom π§)) β (π β π) β (π₯ RingHom π§)) |
22 | 19, 21 | syl6bi 253 |
. . 3
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (π β π) β (π₯ RingHom π§))) |
23 | 22 | imp 408 |
. 2
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π β π) β (π₯ RingHom π§)) |
24 | | eqid 2733 |
. . 3
β’
(RngCatALTVβπ)
= (RngCatALTVβπ) |
25 | | eqid 2733 |
. . 3
β’
(Baseβ(RngCatALTVβπ)) = (Baseβ(RngCatALTVβπ)) |
26 | 7 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β π) |
27 | | eqid 2733 |
. . 3
β’
(compβ(RngCatALTVβπ)) = (compβ(RngCatALTVβπ)) |
28 | | incom 4165 |
. . . . . . . 8
β’ (Ring
β© π) = (π β© Ring) |
29 | | ringrng 46267 |
. . . . . . . . . . 11
β’ (π₯ β Ring β π₯ β Rng) |
30 | 29 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π₯ β Ring β π₯ β Rng)) |
31 | 30 | ssrdv 3954 |
. . . . . . . . 9
β’ (π β Ring β
Rng) |
32 | | sslin 4198 |
. . . . . . . . 9
β’ (Ring
β Rng β (π β©
Ring) β (π β©
Rng)) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
β’ (π β (π β© Ring) β (π β© Rng)) |
34 | 28, 33 | eqsstrid 3996 |
. . . . . . 7
β’ (π β (Ring β© π) β (π β© Rng)) |
35 | 24, 25, 7 | rngcbasALTV 46371 |
. . . . . . 7
β’ (π β
(Baseβ(RngCatALTVβπ)) = (π β© Rng)) |
36 | 34, 9, 35 | 3sstr4d 3995 |
. . . . . 6
β’ (π β π
β (Baseβ(RngCatALTVβπ))) |
37 | 36 | sselda 3948 |
. . . . 5
β’ ((π β§ π₯ β π
) β π₯ β (Baseβ(RngCatALTVβπ))) |
38 | 37 | adantr 482 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π₯ β (Baseβ(RngCatALTVβπ))) |
39 | 38 | adantr 482 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π₯ β (Baseβ(RngCatALTVβπ))) |
40 | 36 | sseld 3947 |
. . . . . . . 8
β’ (π β (π¦ β π
β π¦ β (Baseβ(RngCatALTVβπ)))) |
41 | 40 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π
) β (π¦ β π
β π¦ β (Baseβ(RngCatALTVβπ)))) |
42 | 41 | com12 32 |
. . . . . 6
β’ (π¦ β π
β ((π β§ π₯ β π
) β π¦ β (Baseβ(RngCatALTVβπ)))) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((π¦ β π
β§ π§ β π
) β ((π β§ π₯ β π
) β π¦ β (Baseβ(RngCatALTVβπ)))) |
44 | 43 | impcom 409 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π¦ β (Baseβ(RngCatALTVβπ))) |
45 | 44 | adantr 482 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π¦ β (Baseβ(RngCatALTVβπ))) |
46 | 36 | sseld 3947 |
. . . . . . 7
β’ (π β (π§ β π
β π§ β (Baseβ(RngCatALTVβπ)))) |
47 | 46 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π
) β (π§ β π
β π§ β (Baseβ(RngCatALTVβπ)))) |
48 | 47 | adantld 492 |
. . . . 5
β’ ((π β§ π₯ β π
) β ((π¦ β π
β§ π§ β π
) β π§ β (Baseβ(RngCatALTVβπ)))) |
49 | 48 | imp 408 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π§ β (Baseβ(RngCatALTVβπ))) |
50 | 49 | adantr 482 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π§ β (Baseβ(RngCatALTVβπ))) |
51 | | rhmisrnghm 46308 |
. . . . . . 7
β’ (π β (π₯ RingHom π¦) β π β (π₯ RngHomo π¦)) |
52 | 13, 51 | syl6bi 253 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π₯π»π¦) β π β (π₯ RngHomo π¦))) |
53 | 52 | com12 32 |
. . . . 5
β’ (π β (π₯π»π¦) β (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π β (π₯ RngHomo π¦))) |
54 | 53 | adantr 482 |
. . . 4
β’ ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π β (π₯ RngHomo π¦))) |
55 | 54 | impcom 409 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π₯ RngHomo π¦)) |
56 | | rhmisrnghm 46308 |
. . . . . 6
β’ (π β (π¦ RingHom π§) β π β (π¦ RngHomo π§)) |
57 | 18, 56 | syl6bi 253 |
. . . . 5
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π¦π»π§) β π β (π¦ RngHomo π§))) |
58 | 57 | adantld 492 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β π β (π¦ RngHomo π§))) |
59 | 58 | imp 408 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π¦ RngHomo π§)) |
60 | 24, 25, 26, 27, 39, 45, 50, 55, 59 | rngccoALTV 46376 |
. 2
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatALTVβπ))π§)π) = (π β π)) |
61 | 7, 8, 9, 10 | rhmsubcALTVlem2 46493 |
. . . 4
β’ ((π β§ π₯ β π
β§ π§ β π
) β (π₯π»π§) = (π₯ RingHom π§)) |
62 | 2, 4, 15, 61 | syl3anc 1372 |
. . 3
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π₯π»π§) = (π₯ RingHom π§)) |
63 | 62 | adantr 482 |
. 2
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π₯π»π§) = (π₯ RingHom π§)) |
64 | 23, 60, 63 | 3eltr4d 2849 |
1
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatALTVβπ))π§)π) β (π₯π»π§)) |