Step | Hyp | Ref
| Expression |
1 | | xpcbas.t |
. . . 4
β’ π = (πΆ Γc π·) |
2 | | xpcbas.x |
. . . 4
β’ π = (BaseβπΆ) |
3 | | xpcbas.y |
. . . 4
β’ π = (Baseβπ·) |
4 | | eqid 2733 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
5 | | eqid 2733 |
. . . 4
β’ (Hom
βπ·) = (Hom
βπ·) |
6 | | eqid 2733 |
. . . 4
β’
(compβπΆ) =
(compβπΆ) |
7 | | eqid 2733 |
. . . 4
β’
(compβπ·) =
(compβπ·) |
8 | | simpl 484 |
. . . 4
β’ ((πΆ β V β§ π· β V) β πΆ β V) |
9 | | simpr 486 |
. . . 4
β’ ((πΆ β V β§ π· β V) β π· β V) |
10 | | eqidd 2734 |
. . . 4
β’ ((πΆ β V β§ π· β V) β (π Γ π) = (π Γ π)) |
11 | | eqidd 2734 |
. . . 4
β’ ((πΆ β V β§ π· β V) β (π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£)))) = (π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))) |
12 | | eqidd 2734 |
. . . 4
β’ ((πΆ β V β§ π· β V) β (π₯ β ((π Γ π) Γ (π Γ π)), π¦ β (π Γ π) β¦ (π β ((2nd βπ₯)(π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))π¦), π β ((π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©)) = (π₯ β ((π Γ π) Γ (π Γ π)), π¦ β (π Γ π) β¦ (π β ((2nd βπ₯)(π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))π¦), π β ((π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | xpcval 18070 |
. . 3
β’ ((πΆ β V β§ π· β V) β π = {β¨(Baseβndx),
(π Γ π)β©, β¨(Hom βndx),
(π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))β©, β¨(compβndx), (π₯ β ((π Γ π) Γ (π Γ π)), π¦ β (π Γ π) β¦ (π β ((2nd βπ₯)(π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))π¦), π β ((π’ β (π Γ π), π£ β (π Γ π) β¦ (((1st βπ’)(Hom βπΆ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))β©}) |
14 | 2 | fvexi 6857 |
. . . . 5
β’ π β V |
15 | 3 | fvexi 6857 |
. . . . 5
β’ π β V |
16 | 14, 15 | xpex 7688 |
. . . 4
β’ (π Γ π) β V |
17 | 16 | a1i 11 |
. . 3
β’ ((πΆ β V β§ π· β V) β (π Γ π) β V) |
18 | 13, 17 | estrreslem1 18029 |
. 2
β’ ((πΆ β V β§ π· β V) β (π Γ π) = (Baseβπ)) |
19 | | base0 17093 |
. . 3
β’ β
=
(Baseββ
) |
20 | | fvprc 6835 |
. . . . . 6
β’ (Β¬
πΆ β V β
(BaseβπΆ) =
β
) |
21 | 2, 20 | eqtrid 2785 |
. . . . 5
β’ (Β¬
πΆ β V β π = β
) |
22 | | fvprc 6835 |
. . . . . 6
β’ (Β¬
π· β V β
(Baseβπ·) =
β
) |
23 | 3, 22 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π· β V β π = β
) |
24 | 21, 23 | orim12i 908 |
. . . 4
β’ ((Β¬
πΆ β V β¨ Β¬ π· β V) β (π = β
β¨ π = β
)) |
25 | | ianor 981 |
. . . 4
β’ (Β¬
(πΆ β V β§ π· β V) β (Β¬ πΆ β V β¨ Β¬ π· β V)) |
26 | | xpeq0 6113 |
. . . 4
β’ ((π Γ π) = β
β (π = β
β¨ π = β
)) |
27 | 24, 25, 26 | 3imtr4i 292 |
. . 3
β’ (Β¬
(πΆ β V β§ π· β V) β (π Γ π) = β
) |
28 | | fnxpc 18069 |
. . . . . . 7
β’
Γc Fn (V Γ V) |
29 | | fndm 6606 |
. . . . . . 7
β’ (
Γc Fn (V Γ V) β dom
Γc = (V Γ V)) |
30 | 28, 29 | ax-mp 5 |
. . . . . 6
β’ dom
Γc = (V Γ V) |
31 | 30 | ndmov 7539 |
. . . . 5
β’ (Β¬
(πΆ β V β§ π· β V) β (πΆ Γc
π·) =
β
) |
32 | 1, 31 | eqtrid 2785 |
. . . 4
β’ (Β¬
(πΆ β V β§ π· β V) β π = β
) |
33 | 32 | fveq2d 6847 |
. . 3
β’ (Β¬
(πΆ β V β§ π· β V) β
(Baseβπ) =
(Baseββ
)) |
34 | 19, 27, 33 | 3eqtr4a 2799 |
. 2
β’ (Β¬
(πΆ β V β§ π· β V) β (π Γ π) = (Baseβπ)) |
35 | 18, 34 | pm2.61i 182 |
1
β’ (π Γ π) = (Baseβπ) |