Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . . . 6
β’ ran
(π β π
, π β π β¦ (π Γ π )) = ran (π β π
, π β π β¦ (π Γ π )) |
2 | 1 | txval 13725 |
. . . . 5
β’ ((π
β π β§ π β π) β (π
Γt π) = (topGenβran (π β π
, π β π β¦ (π Γ π )))) |
3 | 2 | adantr 276 |
. . . 4
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π
Γt π) = (topGenβran (π β π
, π β π β¦ (π Γ π )))) |
4 | 3 | oveq1d 5889 |
. . 3
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π
Γt π) βΎt (π΄ Γ π΅)) = ((topGenβran (π β π
, π β π β¦ (π Γ π ))) βΎt (π΄ Γ π΅))) |
5 | 1 | txbasex 13727 |
. . . 4
β’ ((π
β π β§ π β π) β ran (π β π
, π β π β¦ (π Γ π )) β V) |
6 | | xpexg 4740 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β (π΄ Γ π΅) β V) |
7 | | tgrest 13639 |
. . . 4
β’ ((ran
(π β π
, π β π β¦ (π Γ π )) β V β§ (π΄ Γ π΅) β V) β (topGenβ(ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅))) = ((topGenβran (π β π
, π β π β¦ (π Γ π ))) βΎt (π΄ Γ π΅))) |
8 | 5, 6, 7 | syl2an 289 |
. . 3
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (topGenβ(ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅))) = ((topGenβran (π β π
, π β π β¦ (π Γ π ))) βΎt (π΄ Γ π΅))) |
9 | | elrest 12694 |
. . . . . . . 8
β’ ((ran
(π β π
, π β π β¦ (π Γ π )) β V β§ (π΄ Γ π΅) β V) β (π₯ β (ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅)) β βπ€ β ran (π β π
, π β π β¦ (π Γ π ))π₯ = (π€ β© (π΄ Γ π΅)))) |
10 | 5, 6, 9 | syl2an 289 |
. . . . . . 7
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π₯ β (ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅)) β βπ€ β ran (π β π
, π β π β¦ (π Γ π ))π₯ = (π€ β© (π΄ Γ π΅)))) |
11 | | vex 2740 |
. . . . . . . . . . 11
β’ π β V |
12 | 11 | inex1 4137 |
. . . . . . . . . 10
β’ (π β© π΄) β V |
13 | 12 | a1i 9 |
. . . . . . . . 9
β’ ((((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β§ π β π
) β (π β© π΄) β V) |
14 | | elrest 12694 |
. . . . . . . . . 10
β’ ((π
β π β§ π΄ β π) β (π’ β (π
βΎt π΄) β βπ β π
π’ = (π β© π΄))) |
15 | 14 | ad2ant2r 509 |
. . . . . . . . 9
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π’ β (π
βΎt π΄) β βπ β π
π’ = (π β© π΄))) |
16 | | xpeq1 4640 |
. . . . . . . . . . . 12
β’ (π’ = (π β© π΄) β (π’ Γ π£) = ((π β© π΄) Γ π£)) |
17 | 16 | eqeq2d 2189 |
. . . . . . . . . . 11
β’ (π’ = (π β© π΄) β (π₯ = (π’ Γ π£) β π₯ = ((π β© π΄) Γ π£))) |
18 | 17 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π’ = (π β© π΄) β (βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£) β βπ£ β (π βΎt π΅)π₯ = ((π β© π΄) Γ π£))) |
19 | | vex 2740 |
. . . . . . . . . . . . 13
β’ π β V |
20 | 19 | inex1 4137 |
. . . . . . . . . . . 12
β’ (π β© π΅) β V |
21 | 20 | a1i 9 |
. . . . . . . . . . 11
β’ ((((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β§ π β π) β (π β© π΅) β V) |
22 | | elrest 12694 |
. . . . . . . . . . . 12
β’ ((π β π β§ π΅ β π) β (π£ β (π βΎt π΅) β βπ β π π£ = (π β© π΅))) |
23 | 22 | ad2ant2l 508 |
. . . . . . . . . . 11
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π£ β (π βΎt π΅) β βπ β π π£ = (π β© π΅))) |
24 | | xpeq2 4641 |
. . . . . . . . . . . . 13
β’ (π£ = (π β© π΅) β ((π β© π΄) Γ π£) = ((π β© π΄) Γ (π β© π΅))) |
25 | 24 | eqeq2d 2189 |
. . . . . . . . . . . 12
β’ (π£ = (π β© π΅) β (π₯ = ((π β© π΄) Γ π£) β π₯ = ((π β© π΄) Γ (π β© π΅)))) |
26 | 25 | adantl 277 |
. . . . . . . . . . 11
β’ ((((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β§ π£ = (π β© π΅)) β (π₯ = ((π β© π΄) Γ π£) β π₯ = ((π β© π΄) Γ (π β© π΅)))) |
27 | 21, 23, 26 | rexxfr2d 4465 |
. . . . . . . . . 10
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (βπ£ β (π βΎt π΅)π₯ = ((π β© π΄) Γ π£) β βπ β π π₯ = ((π β© π΄) Γ (π β© π΅)))) |
28 | 18, 27 | sylan9bbr 463 |
. . . . . . . . 9
β’ ((((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β§ π’ = (π β© π΄)) β (βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£) β βπ β π π₯ = ((π β© π΄) Γ (π β© π΅)))) |
29 | 13, 15, 28 | rexxfr2d 4465 |
. . . . . . . 8
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (βπ’ β (π
βΎt π΄)βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£) β βπ β π
βπ β π π₯ = ((π β© π΄) Γ (π β© π΅)))) |
30 | 11, 19 | xpex 4741 |
. . . . . . . . . 10
β’ (π Γ π ) β V |
31 | 30 | rgen2w 2533 |
. . . . . . . . 9
β’
βπ β
π
βπ β π (π Γ π ) β V |
32 | | eqid 2177 |
. . . . . . . . . 10
β’ (π β π
, π β π β¦ (π Γ π )) = (π β π
, π β π β¦ (π Γ π )) |
33 | | ineq1 3329 |
. . . . . . . . . . . 12
β’ (π€ = (π Γ π ) β (π€ β© (π΄ Γ π΅)) = ((π Γ π ) β© (π΄ Γ π΅))) |
34 | | inxp 4761 |
. . . . . . . . . . . 12
β’ ((π Γ π ) β© (π΄ Γ π΅)) = ((π β© π΄) Γ (π β© π΅)) |
35 | 33, 34 | eqtrdi 2226 |
. . . . . . . . . . 11
β’ (π€ = (π Γ π ) β (π€ β© (π΄ Γ π΅)) = ((π β© π΄) Γ (π β© π΅))) |
36 | 35 | eqeq2d 2189 |
. . . . . . . . . 10
β’ (π€ = (π Γ π ) β (π₯ = (π€ β© (π΄ Γ π΅)) β π₯ = ((π β© π΄) Γ (π β© π΅)))) |
37 | 32, 36 | rexrnmpo 5989 |
. . . . . . . . 9
β’
(βπ β
π
βπ β π (π Γ π ) β V β (βπ€ β ran (π β π
, π β π β¦ (π Γ π ))π₯ = (π€ β© (π΄ Γ π΅)) β βπ β π
βπ β π π₯ = ((π β© π΄) Γ (π β© π΅)))) |
38 | 31, 37 | ax-mp 5 |
. . . . . . . 8
β’
(βπ€ β ran
(π β π
, π β π β¦ (π Γ π ))π₯ = (π€ β© (π΄ Γ π΅)) β βπ β π
βπ β π π₯ = ((π β© π΄) Γ (π β© π΅))) |
39 | 29, 38 | bitr4di 198 |
. . . . . . 7
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (βπ’ β (π
βΎt π΄)βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£) β βπ€ β ran (π β π
, π β π β¦ (π Γ π ))π₯ = (π€ β© (π΄ Γ π΅)))) |
40 | 10, 39 | bitr4d 191 |
. . . . . 6
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π₯ β (ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅)) β βπ’ β (π
βΎt π΄)βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£))) |
41 | 40 | abbi2dv 2296 |
. . . . 5
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅)) = {π₯ β£ βπ’ β (π
βΎt π΄)βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£)}) |
42 | | eqid 2177 |
. . . . . 6
β’ (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)) = (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)) |
43 | 42 | rnmpo 5984 |
. . . . 5
β’ ran
(π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)) = {π₯ β£ βπ’ β (π
βΎt π΄)βπ£ β (π βΎt π΅)π₯ = (π’ Γ π£)} |
44 | 41, 43 | eqtr4di 2228 |
. . . 4
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅)) = ran (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£))) |
45 | 44 | fveq2d 5519 |
. . 3
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (topGenβ(ran (π β π
, π β π β¦ (π Γ π )) βΎt (π΄ Γ π΅))) = (topGenβran (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)))) |
46 | 4, 8, 45 | 3eqtr2d 2216 |
. 2
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π
Γt π) βΎt (π΄ Γ π΅)) = (topGenβran (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)))) |
47 | | restfn 12691 |
. . . 4
β’
βΎt Fn (V Γ V) |
48 | | simpll 527 |
. . . . 5
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π
β π) |
49 | 48 | elexd 2750 |
. . . 4
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π
β V) |
50 | | simprl 529 |
. . . . 5
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
51 | 50 | elexd 2750 |
. . . 4
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π΄ β V) |
52 | | fnovex 5907 |
. . . 4
β’ ((
βΎt Fn (V Γ V) β§ π
β V β§ π΄ β V) β (π
βΎt π΄) β V) |
53 | 47, 49, 51, 52 | mp3an2i 1342 |
. . 3
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π
βΎt π΄) β V) |
54 | | simplr 528 |
. . . . 5
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π β π) |
55 | 54 | elexd 2750 |
. . . 4
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π β V) |
56 | | simprr 531 |
. . . . 5
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
57 | 56 | elexd 2750 |
. . . 4
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π΅ β V) |
58 | | fnovex 5907 |
. . . 4
β’ ((
βΎt Fn (V Γ V) β§ π β V β§ π΅ β V) β (π βΎt π΅) β V) |
59 | 47, 55, 57, 58 | mp3an2i 1342 |
. . 3
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π βΎt π΅) β V) |
60 | | eqid 2177 |
. . . 4
β’ ran
(π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)) = ran (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)) |
61 | 60 | txval 13725 |
. . 3
β’ (((π
βΎt π΄) β V β§ (π βΎt π΅) β V) β ((π
βΎt π΄) Γt (π βΎt π΅)) = (topGenβran (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)))) |
62 | 53, 59, 61 | syl2anc 411 |
. 2
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π
βΎt π΄) Γt (π βΎt π΅)) = (topGenβran (π’ β (π
βΎt π΄), π£ β (π βΎt π΅) β¦ (π’ Γ π£)))) |
63 | 46, 62 | eqtr4d 2213 |
1
β’ (((π
β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π
Γt π) βΎt (π΄ Γ π΅)) = ((π
βΎt π΄) Γt (π βΎt π΅))) |