Step | Hyp | Ref
| Expression |
1 | | ringcbasALTV.c |
. . . 4
β’ πΆ = (RingCatALTVβπ) |
2 | | ringcbasALTV.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
3 | | ringcbasALTV.u |
. . . 4
β’ (π β π β π) |
4 | | ringccoALTV.o |
. . . 4
β’ Β· =
(compβπΆ) |
5 | 1, 2, 3, 4 | ringccofvalALTV 46249 |
. . 3
β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))) |
6 | | simprl 769 |
. . . . . . 7
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β π£ = β¨π, πβ©) |
7 | 6 | fveq2d 6843 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd βπ£) = (2nd
ββ¨π, πβ©)) |
8 | | ringccoALTV.x |
. . . . . . . 8
β’ (π β π β π΅) |
9 | | ringccoALTV.y |
. . . . . . . 8
β’ (π β π β π΅) |
10 | | op2ndg 7926 |
. . . . . . . 8
β’ ((π β π΅ β§ π β π΅) β (2nd ββ¨π, πβ©) = π) |
11 | 8, 9, 10 | syl2anc 584 |
. . . . . . 7
β’ (π β (2nd
ββ¨π, πβ©) = π) |
12 | 11 | adantr 481 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd ββ¨π, πβ©) = π) |
13 | 7, 12 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd βπ£) = π) |
14 | | simprr 771 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β π§ = π) |
15 | 13, 14 | oveq12d 7369 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β ((2nd βπ£) RingHom π§) = (π RingHom π)) |
16 | 6 | fveq2d 6843 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st βπ£) = (1st
ββ¨π, πβ©)) |
17 | | op1stg 7925 |
. . . . . . . 8
β’ ((π β π΅ β§ π β π΅) β (1st ββ¨π, πβ©) = π) |
18 | 8, 9, 17 | syl2anc 584 |
. . . . . . 7
β’ (π β (1st
ββ¨π, πβ©) = π) |
19 | 18 | adantr 481 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st ββ¨π, πβ©) = π) |
20 | 16, 19 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st βπ£) = π) |
21 | 20, 13 | oveq12d 7369 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β ((1st βπ£) RingHom (2nd
βπ£)) = (π RingHom π)) |
22 | | eqidd 2738 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π β π) = (π β π)) |
23 | 15, 21, 22 | mpoeq123dv 7426 |
. . 3
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)) = (π β (π RingHom π), π β (π RingHom π) β¦ (π β π))) |
24 | | opelxpi 5668 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) |
25 | 8, 9, 24 | syl2anc 584 |
. . 3
β’ (π β β¨π, πβ© β (π΅ Γ π΅)) |
26 | | ringccoALTV.z |
. . 3
β’ (π β π β π΅) |
27 | | ovex 7384 |
. . . . 5
β’ (π RingHom π) β V |
28 | | ovex 7384 |
. . . . 5
β’ (π RingHom π) β V |
29 | 27, 28 | mpoex 8004 |
. . . 4
β’ (π β (π RingHom π), π β (π RingHom π) β¦ (π β π)) β V |
30 | 29 | a1i 11 |
. . 3
β’ (π β (π β (π RingHom π), π β (π RingHom π) β¦ (π β π)) β V) |
31 | 5, 23, 25, 26, 30 | ovmpod 7501 |
. 2
β’ (π β (β¨π, πβ© Β· π) = (π β (π RingHom π), π β (π RingHom π) β¦ (π β π))) |
32 | | simprl 769 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΊ) |
33 | | simprr 771 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΉ) |
34 | 32, 33 | coeq12d 5818 |
. 2
β’ ((π β§ (π = πΊ β§ π = πΉ)) β (π β π) = (πΊ β πΉ)) |
35 | | ringccoALTV.g |
. 2
β’ (π β πΊ β (π RingHom π)) |
36 | | ringccoALTV.f |
. 2
β’ (π β πΉ β (π RingHom π)) |
37 | | coexg 7858 |
. . 3
β’ ((πΊ β (π RingHom π) β§ πΉ β (π RingHom π)) β (πΊ β πΉ) β V) |
38 | 35, 36, 37 | syl2anc 584 |
. 2
β’ (π β (πΊ β πΉ) β V) |
39 | 31, 34, 35, 36, 38 | ovmpod 7501 |
1
β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) |