Step | Hyp | Ref
| Expression |
1 | | rngcbasALTV.c |
. . . 4
β’ πΆ = (RngCatALTVβπ) |
2 | | rngcbasALTV.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
3 | | rngcbasALTV.u |
. . . 4
β’ (π β π β π) |
4 | | rngccofvalALTV.o |
. . . 4
β’ Β· =
(compβπΆ) |
5 | 1, 2, 3, 4 | rngccofvalALTV 47225 |
. . 3
β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHom π§), π β ((1st βπ£) RngHom (2nd
βπ£)) β¦ (π β π)))) |
6 | | simprl 768 |
. . . . . . 7
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β π£ = β¨π, πβ©) |
7 | 6 | fveq2d 6889 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd βπ£) = (2nd
ββ¨π, πβ©)) |
8 | | rngccoALTV.x |
. . . . . . . 8
β’ (π β π β π΅) |
9 | | rngccoALTV.y |
. . . . . . . 8
β’ (π β π β π΅) |
10 | | op2ndg 7987 |
. . . . . . . 8
β’ ((π β π΅ β§ π β π΅) β (2nd ββ¨π, πβ©) = π) |
11 | 8, 9, 10 | syl2anc 583 |
. . . . . . 7
β’ (π β (2nd
ββ¨π, πβ©) = π) |
12 | 11 | adantr 480 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd ββ¨π, πβ©) = π) |
13 | 7, 12 | eqtrd 2766 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd βπ£) = π) |
14 | | simprr 770 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β π§ = π) |
15 | 13, 14 | oveq12d 7423 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β ((2nd βπ£) RngHom π§) = (π RngHom π)) |
16 | 6 | fveq2d 6889 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st βπ£) = (1st
ββ¨π, πβ©)) |
17 | | op1stg 7986 |
. . . . . . . 8
β’ ((π β π΅ β§ π β π΅) β (1st ββ¨π, πβ©) = π) |
18 | 8, 9, 17 | syl2anc 583 |
. . . . . . 7
β’ (π β (1st
ββ¨π, πβ©) = π) |
19 | 18 | adantr 480 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st ββ¨π, πβ©) = π) |
20 | 16, 19 | eqtrd 2766 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st βπ£) = π) |
21 | 20, 13 | oveq12d 7423 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β ((1st βπ£) RngHom (2nd
βπ£)) = (π RngHom π)) |
22 | | eqidd 2727 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π β π) = (π β π)) |
23 | 15, 21, 22 | mpoeq123dv 7480 |
. . 3
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π β ((2nd βπ£) RngHom π§), π β ((1st βπ£) RngHom (2nd
βπ£)) β¦ (π β π)) = (π β (π RngHom π), π β (π RngHom π) β¦ (π β π))) |
24 | | opelxpi 5706 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) |
25 | 8, 9, 24 | syl2anc 583 |
. . 3
β’ (π β β¨π, πβ© β (π΅ Γ π΅)) |
26 | | rngccoALTV.z |
. . 3
β’ (π β π β π΅) |
27 | | ovex 7438 |
. . . . 5
β’ (π RngHom π) β V |
28 | | ovex 7438 |
. . . . 5
β’ (π RngHom π) β V |
29 | 27, 28 | mpoex 8065 |
. . . 4
β’ (π β (π RngHom π), π β (π RngHom π) β¦ (π β π)) β V |
30 | 29 | a1i 11 |
. . 3
β’ (π β (π β (π RngHom π), π β (π RngHom π) β¦ (π β π)) β V) |
31 | 5, 23, 25, 26, 30 | ovmpod 7556 |
. 2
β’ (π β (β¨π, πβ© Β· π) = (π β (π RngHom π), π β (π RngHom π) β¦ (π β π))) |
32 | | simprl 768 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΊ) |
33 | | simprr 770 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΉ) |
34 | 32, 33 | coeq12d 5858 |
. 2
β’ ((π β§ (π = πΊ β§ π = πΉ)) β (π β π) = (πΊ β πΉ)) |
35 | | rngccoALTV.g |
. 2
β’ (π β πΊ β (π RngHom π)) |
36 | | rngccoALTV.f |
. 2
β’ (π β πΉ β (π RngHom π)) |
37 | | coexg 7919 |
. . 3
β’ ((πΊ β (π RngHom π) β§ πΉ β (π RngHom π)) β (πΊ β πΉ) β V) |
38 | 35, 36, 37 | syl2anc 583 |
. 2
β’ (π β (πΊ β πΉ) β V) |
39 | 31, 34, 35, 36, 38 | ovmpod 7556 |
1
β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) |