Step | Hyp | Ref
| Expression |
1 | | rngcval.c |
. 2
β’ πΆ = (RngCatβπ) |
2 | | df-rngc 46410 |
. . 3
β’ RngCat =
(π’ β V β¦
((ExtStrCatβπ’)
βΎcat ( RngHomo βΎ ((π’ β© Rng) Γ (π’ β© Rng))))) |
3 | | fveq2 6862 |
. . . . 5
β’ (π’ = π β (ExtStrCatβπ’) = (ExtStrCatβπ)) |
4 | 3 | adantl 482 |
. . . 4
β’ ((π β§ π’ = π) β (ExtStrCatβπ’) = (ExtStrCatβπ)) |
5 | | ineq1 4185 |
. . . . . . . 8
β’ (π’ = π β (π’ β© Rng) = (π β© Rng)) |
6 | 5 | sqxpeqd 5685 |
. . . . . . 7
β’ (π’ = π β ((π’ β© Rng) Γ (π’ β© Rng)) = ((π β© Rng) Γ (π β© Rng))) |
7 | | rngcval.b |
. . . . . . . . 9
β’ (π β π΅ = (π β© Rng)) |
8 | 7 | sqxpeqd 5685 |
. . . . . . . 8
β’ (π β (π΅ Γ π΅) = ((π β© Rng) Γ (π β© Rng))) |
9 | 8 | eqcomd 2737 |
. . . . . . 7
β’ (π β ((π β© Rng) Γ (π β© Rng)) = (π΅ Γ π΅)) |
10 | 6, 9 | sylan9eqr 2793 |
. . . . . 6
β’ ((π β§ π’ = π) β ((π’ β© Rng) Γ (π’ β© Rng)) = (π΅ Γ π΅)) |
11 | 10 | reseq2d 5957 |
. . . . 5
β’ ((π β§ π’ = π) β ( RngHomo βΎ ((π’ β© Rng) Γ (π’ β© Rng))) = ( RngHomo
βΎ (π΅ Γ π΅))) |
12 | | rngcval.h |
. . . . . . 7
β’ (π β π» = ( RngHomo βΎ (π΅ Γ π΅))) |
13 | 12 | eqcomd 2737 |
. . . . . 6
β’ (π β ( RngHomo βΎ (π΅ Γ π΅)) = π») |
14 | 13 | adantr 481 |
. . . . 5
β’ ((π β§ π’ = π) β ( RngHomo βΎ (π΅ Γ π΅)) = π») |
15 | 11, 14 | eqtrd 2771 |
. . . 4
β’ ((π β§ π’ = π) β ( RngHomo βΎ ((π’ β© Rng) Γ (π’ β© Rng))) = π») |
16 | 4, 15 | oveq12d 7395 |
. . 3
β’ ((π β§ π’ = π) β ((ExtStrCatβπ’) βΎcat (
RngHomo βΎ ((π’ β©
Rng) Γ (π’ β©
Rng)))) = ((ExtStrCatβπ) βΎcat π»)) |
17 | | rngcval.u |
. . . 4
β’ (π β π β π) |
18 | 17 | elexd 3479 |
. . 3
β’ (π β π β V) |
19 | | ovexd 7412 |
. . 3
β’ (π β ((ExtStrCatβπ) βΎcat π») β V) |
20 | 2, 16, 18, 19 | fvmptd2 6976 |
. 2
β’ (π β (RngCatβπ) = ((ExtStrCatβπ) βΎcat π»)) |
21 | 1, 20 | eqtrid 2783 |
1
β’ (π β πΆ = ((ExtStrCatβπ) βΎcat π»)) |