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 | | rngcrescrhm.u |
. . . . . . . 8
β’ (π β π β π) |
8 | | rngcrescrhm.c |
. . . . . . . 8
β’ πΆ = (RngCatβπ) |
9 | | rngcrescrhm.r |
. . . . . . . 8
β’ (π β π
= (Ring β© π)) |
10 | | rngcrescrhm.h |
. . . . . . . 8
β’ π» = ( RingHom βΎ (π
Γ π
)) |
11 | 7, 8, 9, 10 | rhmsubclem2 46459 |
. . . . . . 7
β’ ((π β§ π₯ β π
β§ π¦ β π
) β (π₯π»π¦) = (π₯ RingHom π¦)) |
12 | 2, 4, 6, 11 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π₯π»π¦) = (π₯ RingHom π¦)) |
13 | 12 | eleq2d 2824 |
. . . . 5
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π₯π»π¦) β π β (π₯ RingHom π¦))) |
14 | | simpr 486 |
. . . . . . . 8
β’ ((π¦ β π
β§ π§ β π
) β π§ β π
) |
15 | 14 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π§ β π
) |
16 | 7, 8, 9, 10 | rhmsubclem2 46459 |
. . . . . . 7
β’ ((π β§ π¦ β π
β§ π§ β π
) β (π¦π»π§) = (π¦ RingHom π§)) |
17 | 2, 6, 15, 16 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π¦π»π§) = (π¦ RingHom π§)) |
18 | 17 | eleq2d 2824 |
. . . . 5
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π¦π»π§) β π β (π¦ RingHom π§))) |
19 | 13, 18 | anbi12d 632 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (π β (π₯ RingHom π¦) β§ π β (π¦ RingHom π§)))) |
20 | | rhmco 20180 |
. . . . 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 | 7 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β π) |
25 | 8 | eqcomi 2746 |
. . . 4
β’
(RngCatβπ) =
πΆ |
26 | 25 | fveq2i 6850 |
. . 3
β’
(compβ(RngCatβπ)) = (compβπΆ) |
27 | | inss2 4194 |
. . . . . . 7
β’ (Ring
β© π) β π |
28 | 9, 27 | eqsstrdi 4003 |
. . . . . 6
β’ (π β π
β π) |
29 | 28 | sselda 3949 |
. . . . 5
β’ ((π β§ π₯ β π
) β π₯ β π) |
30 | 29 | adantr 482 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π₯ β π) |
31 | 30 | adantr 482 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π₯ β π) |
32 | 28 | sseld 3948 |
. . . . . . 7
β’ (π β (π¦ β π
β π¦ β π)) |
33 | 32 | adantrd 493 |
. . . . . 6
β’ (π β ((π¦ β π
β§ π§ β π
) β π¦ β π)) |
34 | 33 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π
) β ((π¦ β π
β§ π§ β π
) β π¦ β π)) |
35 | 34 | imp 408 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π¦ β π) |
36 | 35 | adantr 482 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π¦ β π) |
37 | 28 | sseld 3948 |
. . . . . . 7
β’ (π β (π§ β π
β π§ β π)) |
38 | 37 | adantld 492 |
. . . . . 6
β’ (π β ((π¦ β π
β§ π§ β π
) β π§ β π)) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π
) β ((π¦ β π
β§ π§ β π
) β π§ β π)) |
40 | 39 | imp 408 |
. . . 4
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π§ β π) |
41 | 40 | adantr 482 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π§ β π) |
42 | 10 | oveqi 7375 |
. . . . . . . . 9
β’ (π₯π»π¦) = (π₯( RingHom βΎ (π
Γ π
))π¦) |
43 | 4, 6 | ovresd 7526 |
. . . . . . . . 9
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π₯( RingHom βΎ (π
Γ π
))π¦) = (π₯ RingHom π¦)) |
44 | 42, 43 | eqtrid 2789 |
. . . . . . . 8
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π₯π»π¦) = (π₯ RingHom π¦)) |
45 | 44 | eleq2d 2824 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π₯π»π¦) β π β (π₯ RingHom π¦))) |
46 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ₯) =
(Baseβπ₯) |
47 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ¦) =
(Baseβπ¦) |
48 | 46, 47 | rhmf 20167 |
. . . . . . 7
β’ (π β (π₯ RingHom π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
49 | 45, 48 | syl6bi 253 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
50 | 49 | com12 32 |
. . . . 5
β’ (π β (π₯π»π¦) β (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
51 | 50 | adantr 482 |
. . . 4
β’ ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
52 | 51 | impcom 409 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
53 | 10 | oveqi 7375 |
. . . . . . . . 9
β’ (π¦π»π§) = (π¦( RingHom βΎ (π
Γ π
))π§) |
54 | | ovres 7525 |
. . . . . . . . . 10
β’ ((π¦ β π
β§ π§ β π
) β (π¦( RingHom βΎ (π
Γ π
))π§) = (π¦ RingHom π§)) |
55 | 54 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π¦( RingHom βΎ (π
Γ π
))π§) = (π¦ RingHom π§)) |
56 | 53, 55 | eqtrid 2789 |
. . . . . . . 8
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π¦π»π§) = (π¦ RingHom π§)) |
57 | 56 | eleq2d 2824 |
. . . . . . 7
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π¦π»π§) β π β (π¦ RingHom π§))) |
58 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ§) =
(Baseβπ§) |
59 | 47, 58 | rhmf 20167 |
. . . . . . 7
β’ (π β (π¦ RingHom π§) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
60 | 57, 59 | syl6bi 253 |
. . . . . 6
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π β (π¦π»π§) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
61 | 60 | com12 32 |
. . . . 5
β’ (π β (π¦π»π§) β (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
62 | 61 | adantl 483 |
. . . 4
β’ ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
63 | 62 | impcom 409 |
. . 3
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
64 | 8, 24, 26, 31, 36, 41, 52, 63 | rngcco 46343 |
. 2
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) = (π β π)) |
65 | 7, 8, 9, 10 | rhmsubclem2 46459 |
. . . 4
β’ ((π β§ π₯ β π
β§ π§ β π
) β (π₯π»π§) = (π₯ RingHom π§)) |
66 | 2, 4, 15, 65 | syl3anc 1372 |
. . 3
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β (π₯π»π§) = (π₯ RingHom π§)) |
67 | 66 | adantr 482 |
. 2
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π₯π»π§) = (π₯ RingHom π§)) |
68 | 23, 64, 67 | 3eltr4d 2853 |
1
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) |