Step | Hyp | Ref
| Expression |
1 | | vex 3450 |
. . . . . . 7
β’ π β V |
2 | | vex 3450 |
. . . . . . 7
β’ π β V |
3 | 1, 2 | prss 4781 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β {π, π} β π΅) |
4 | | pwsle.v |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
5 | | pwsle.y |
. . . . . . . . . 10
β’ π = (π
βs πΌ) |
6 | | eqid 2737 |
. . . . . . . . . 10
β’
(Scalarβπ
) =
(Scalarβπ
) |
7 | 5, 6 | pwsval 17369 |
. . . . . . . . 9
β’ ((π
β π β§ πΌ β π) β π = ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
8 | 7 | fveq2d 6847 |
. . . . . . . 8
β’ ((π
β π β§ πΌ β π) β (Baseβπ) = (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
9 | 4, 8 | eqtrid 2789 |
. . . . . . 7
β’ ((π
β π β§ πΌ β π) β π΅ = (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
10 | 9 | sseq2d 3977 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β ({π, π} β π΅ β {π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))))) |
11 | 3, 10 | bitrid 283 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β ((π β π΅ β§ π β π΅) β {π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))))) |
12 | 11 | anbi1d 631 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯)) β ({π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯)))) |
13 | | fvconst2g 7152 |
. . . . . . . . . . . 12
β’ ((π
β π β§ π₯ β πΌ) β ((πΌ Γ {π
})βπ₯) = π
) |
14 | 13 | ad4ant14 751 |
. . . . . . . . . . 11
β’ ((((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β ((πΌ Γ {π
})βπ₯) = π
) |
15 | 14 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (leβ((πΌ Γ {π
})βπ₯)) = (leβπ
)) |
16 | | pwsle.o |
. . . . . . . . . 10
β’ π = (leβπ
) |
17 | 15, 16 | eqtr4di 2795 |
. . . . . . . . 9
β’ ((((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (leβ((πΌ Γ {π
})βπ₯)) = π) |
18 | 17 | breqd 5117 |
. . . . . . . 8
β’ ((((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β ((πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯) β (πβπ₯)π(πβπ₯))) |
19 | 18 | ralbidva 3173 |
. . . . . . 7
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β (βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯) β βπ₯ β πΌ (πβπ₯)π(πβπ₯))) |
20 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
21 | | simpll 766 |
. . . . . . . . . 10
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π
β π) |
22 | | simplr 768 |
. . . . . . . . . 10
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β πΌ β π) |
23 | | simprl 770 |
. . . . . . . . . 10
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π β π΅) |
24 | 5, 20, 4, 21, 22, 23 | pwselbas 17372 |
. . . . . . . . 9
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π:πΌβΆ(Baseβπ
)) |
25 | 24 | ffnd 6670 |
. . . . . . . 8
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π Fn πΌ) |
26 | | simprr 772 |
. . . . . . . . . 10
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π β π΅) |
27 | 5, 20, 4, 21, 22, 26 | pwselbas 17372 |
. . . . . . . . 9
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π:πΌβΆ(Baseβπ
)) |
28 | 27 | ffnd 6670 |
. . . . . . . 8
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β π Fn πΌ) |
29 | | inidm 4179 |
. . . . . . . 8
β’ (πΌ β© πΌ) = πΌ |
30 | | eqidd 2738 |
. . . . . . . 8
β’ ((((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (πβπ₯) = (πβπ₯)) |
31 | | eqidd 2738 |
. . . . . . . 8
β’ ((((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (πβπ₯) = (πβπ₯)) |
32 | 25, 28, 23, 26, 29, 30, 31 | ofrfvalg 7626 |
. . . . . . 7
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β (π βr ππ β βπ₯ β πΌ (πβπ₯)π(πβπ₯))) |
33 | 19, 32 | bitr4d 282 |
. . . . . 6
β’ (((π
β π β§ πΌ β π) β§ (π β π΅ β§ π β π΅)) β (βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯) β π βr ππ)) |
34 | 33 | pm5.32da 580 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β (((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯)) β ((π β π΅ β§ π β π΅) β§ π βr ππ))) |
35 | | brinxp2 5710 |
. . . . 5
β’ (π( βr π β© (π΅ Γ π΅))π β ((π β π΅ β§ π β π΅) β§ π βr ππ)) |
36 | 34, 35 | bitr4di 289 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (((π β π΅ β§ π β π΅) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯)) β π( βr π β© (π΅ Γ π΅))π)) |
37 | 12, 36 | bitr3d 281 |
. . 3
β’ ((π
β π β§ πΌ β π) β (({π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯)) β π( βr π β© (π΅ Γ π΅))π)) |
38 | 37 | opabbidv 5172 |
. 2
β’ ((π
β π β§ πΌ β π) β {β¨π, πβ© β£ ({π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯))} = {β¨π, πβ© β£ π( βr π β© (π΅ Γ π΅))π}) |
39 | | pwsle.l |
. . . 4
β’ β€ =
(leβπ) |
40 | 7 | fveq2d 6847 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (leβπ) = (leβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
41 | 39, 40 | eqtrid 2789 |
. . 3
β’ ((π
β π β§ πΌ β π) β β€ =
(leβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
42 | | eqid 2737 |
. . . 4
β’
((Scalarβπ
)Xs(πΌ Γ {π
})) = ((Scalarβπ
)Xs(πΌ Γ {π
})) |
43 | | fvexd 6858 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (Scalarβπ
) β V) |
44 | | simpr 486 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β πΌ β π) |
45 | | snex 5389 |
. . . . 5
β’ {π
} β V |
46 | | xpexg 7685 |
. . . . 5
β’ ((πΌ β π β§ {π
} β V) β (πΌ Γ {π
}) β V) |
47 | 44, 45, 46 | sylancl 587 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (πΌ Γ {π
}) β V) |
48 | | eqid 2737 |
. . . 4
β’
(Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) = (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
49 | | snnzg 4736 |
. . . . . 6
β’ (π
β π β {π
} β β
) |
50 | 49 | adantr 482 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β {π
} β β
) |
51 | | dmxp 5885 |
. . . . 5
β’ ({π
} β β
β dom (πΌ Γ {π
}) = πΌ) |
52 | 50, 51 | syl 17 |
. . . 4
β’ ((π
β π β§ πΌ β π) β dom (πΌ Γ {π
}) = πΌ) |
53 | | eqid 2737 |
. . . 4
β’
(leβ((Scalarβπ
)Xs(πΌ Γ {π
}))) = (leβ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
54 | 42, 43, 47, 48, 52, 53 | prdsle 17345 |
. . 3
β’ ((π
β π β§ πΌ β π) β (leβ((Scalarβπ
)Xs(πΌ Γ {π
}))) = {β¨π, πβ© β£ ({π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯))}) |
55 | 41, 54 | eqtrd 2777 |
. 2
β’ ((π
β π β§ πΌ β π) β β€ = {β¨π, πβ© β£ ({π, π} β (Baseβ((Scalarβπ
)Xs(πΌ Γ {π
}))) β§ βπ₯ β πΌ (πβπ₯)(leβ((πΌ Γ {π
})βπ₯))(πβπ₯))}) |
56 | | relinxp 5771 |
. . . 4
β’ Rel (
βr π β©
(π΅ Γ π΅)) |
57 | 56 | a1i 11 |
. . 3
β’ ((π
β π β§ πΌ β π) β Rel ( βr π β© (π΅ Γ π΅))) |
58 | | dfrel4v 6143 |
. . 3
β’ (Rel (
βr π β©
(π΅ Γ π΅)) β ( βr
π β© (π΅ Γ π΅)) = {β¨π, πβ© β£ π( βr π β© (π΅ Γ π΅))π}) |
59 | 57, 58 | sylib 217 |
. 2
β’ ((π
β π β§ πΌ β π) β ( βr π β© (π΅ Γ π΅)) = {β¨π, πβ© β£ π( βr π β© (π΅ Γ π΅))π}) |
60 | 38, 55, 59 | 3eqtr4d 2787 |
1
β’ ((π
β π β§ πΌ β π) β β€ = ( βr
π β© (π΅ Γ π΅))) |