Step | Hyp | Ref
| Expression |
1 | | ringcval.c |
. 2
β’ πΆ = (RingCatβπ) |
2 | | df-ringc 46903 |
. . 3
β’ RingCat =
(π’ β V β¦
((ExtStrCatβπ’)
βΎcat ( RingHom βΎ ((π’ β© Ring) Γ (π’ β© Ring))))) |
3 | | fveq2 6892 |
. . . . 5
β’ (π’ = π β (ExtStrCatβπ’) = (ExtStrCatβπ)) |
4 | 3 | adantl 483 |
. . . 4
β’ ((π β§ π’ = π) β (ExtStrCatβπ’) = (ExtStrCatβπ)) |
5 | | ineq1 4206 |
. . . . . . . 8
β’ (π’ = π β (π’ β© Ring) = (π β© Ring)) |
6 | 5 | sqxpeqd 5709 |
. . . . . . 7
β’ (π’ = π β ((π’ β© Ring) Γ (π’ β© Ring)) = ((π β© Ring) Γ (π β© Ring))) |
7 | | ringcval.b |
. . . . . . . . 9
β’ (π β π΅ = (π β© Ring)) |
8 | 7 | sqxpeqd 5709 |
. . . . . . . 8
β’ (π β (π΅ Γ π΅) = ((π β© Ring) Γ (π β© Ring))) |
9 | 8 | eqcomd 2739 |
. . . . . . 7
β’ (π β ((π β© Ring) Γ (π β© Ring)) = (π΅ Γ π΅)) |
10 | 6, 9 | sylan9eqr 2795 |
. . . . . 6
β’ ((π β§ π’ = π) β ((π’ β© Ring) Γ (π’ β© Ring)) = (π΅ Γ π΅)) |
11 | 10 | reseq2d 5982 |
. . . . 5
β’ ((π β§ π’ = π) β ( RingHom βΎ ((π’ β© Ring) Γ (π’ β© Ring))) = ( RingHom
βΎ (π΅ Γ π΅))) |
12 | | ringcval.h |
. . . . . . 7
β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) |
13 | 12 | eqcomd 2739 |
. . . . . 6
β’ (π β ( RingHom βΎ (π΅ Γ π΅)) = π») |
14 | 13 | adantr 482 |
. . . . 5
β’ ((π β§ π’ = π) β ( RingHom βΎ (π΅ Γ π΅)) = π») |
15 | 11, 14 | eqtrd 2773 |
. . . 4
β’ ((π β§ π’ = π) β ( RingHom βΎ ((π’ β© Ring) Γ (π’ β© Ring))) = π») |
16 | 4, 15 | oveq12d 7427 |
. . 3
β’ ((π β§ π’ = π) β ((ExtStrCatβπ’) βΎcat (
RingHom βΎ ((π’ β©
Ring) Γ (π’ β©
Ring)))) = ((ExtStrCatβπ) βΎcat π»)) |
17 | | ringcval.u |
. . . 4
β’ (π β π β π) |
18 | 17 | elexd 3495 |
. . 3
β’ (π β π β V) |
19 | | ovexd 7444 |
. . 3
β’ (π β ((ExtStrCatβπ) βΎcat π») β V) |
20 | 2, 16, 18, 19 | fvmptd2 7007 |
. 2
β’ (π β (RingCatβπ) = ((ExtStrCatβπ) βΎcat π»)) |
21 | 1, 20 | eqtrid 2785 |
1
β’ (π β πΆ = ((ExtStrCatβπ) βΎcat π»)) |