Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΎ β HL β§ π β π»)) |
2 | | ssrab2 4042 |
. . . 4
β’ {π₯ β π΅ β£ π β (πΌβπ₯)} β π΅ |
3 | 2 | a1i 11 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β {π₯ β π΅ β£ π β (πΌβπ₯)} β π΅) |
4 | | hlop 37853 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OP) |
5 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΎ β OP) |
6 | | dihglb.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
7 | | eqid 2737 |
. . . . . . 7
β’
(1.βπΎ) =
(1.βπΎ) |
8 | 6, 7 | op1cl 37676 |
. . . . . 6
β’ (πΎ β OP β
(1.βπΎ) β π΅) |
9 | 5, 8 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (1.βπΎ) β π΅) |
10 | | simpr 486 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β π) |
11 | | dihglb.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
12 | | dihglb.i |
. . . . . . . 8
β’ πΌ = ((DIsoHβπΎ)βπ) |
13 | | dihglb2.u |
. . . . . . . 8
β’ π = ((DVecHβπΎ)βπ) |
14 | | dihglb2.v |
. . . . . . . 8
β’ π = (Baseβπ) |
15 | 7, 11, 12, 13, 14 | dih1 39778 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (πΌβ(1.βπΎ)) = π) |
16 | 15 | adantr 482 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(1.βπΎ)) = π) |
17 | 10, 16 | sseqtrrd 3990 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β (πΌβ(1.βπΎ))) |
18 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = (1.βπΎ) β (πΌβπ₯) = (πΌβ(1.βπΎ))) |
19 | 18 | sseq2d 3981 |
. . . . . 6
β’ (π₯ = (1.βπΎ) β (π β (πΌβπ₯) β π β (πΌβ(1.βπΎ)))) |
20 | 19 | elrab 3650 |
. . . . 5
β’
((1.βπΎ) β
{π₯ β π΅ β£ π β (πΌβπ₯)} β ((1.βπΎ) β π΅ β§ π β (πΌβ(1.βπΎ)))) |
21 | 9, 17, 20 | sylanbrc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (1.βπΎ) β {π₯ β π΅ β£ π β (πΌβπ₯)}) |
22 | 21 | ne0d 4300 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β {π₯ β π΅ β£ π β (πΌβπ₯)} β β
) |
23 | | dihglb.g |
. . . 4
β’ πΊ = (glbβπΎ) |
24 | 6, 23, 11, 12 | dihglb 39833 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ({π₯ β π΅ β£ π β (πΌβπ₯)} β π΅ β§ {π₯ β π΅ β£ π β (πΌβπ₯)} β β
)) β (πΌβ(πΊβ{π₯ β π΅ β£ π β (πΌβπ₯)})) = β©
π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} (πΌβπ§)) |
25 | 1, 3, 22, 24 | syl12anc 836 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(πΊβ{π₯ β π΅ β£ π β (πΌβπ₯)})) = β©
π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} (πΌβπ§)) |
26 | | fvex 6860 |
. . . 4
β’ (πΌβπ§) β V |
27 | 26 | dfiin2 4999 |
. . 3
β’ β© π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} (πΌβπ§) = β© {π¦ β£ βπ§ β {π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§)} |
28 | 6, 11, 12 | dihfn 39760 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π») β πΌ Fn π΅) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ π β π) β§ π β π¦) β πΌ Fn π΅) |
30 | | fvelrnb 6908 |
. . . . . . . . . . 11
β’ (πΌ Fn π΅ β (π¦ β ran πΌ β βπ§ β π΅ (πΌβπ§) = π¦)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ π β π) β§ π β π¦) β (π¦ β ran πΌ β βπ§ β π΅ (πΌβπ§) = π¦)) |
32 | | eqcom 2744 |
. . . . . . . . . . . 12
β’ ((πΌβπ§) = π¦ β π¦ = (πΌβπ§)) |
33 | 32 | rexbii 3098 |
. . . . . . . . . . 11
β’
(βπ§ β
π΅ (πΌβπ§) = π¦ β βπ§ β π΅ π¦ = (πΌβπ§)) |
34 | | df-rex 3075 |
. . . . . . . . . . 11
β’
(βπ§ β
π΅ π¦ = (πΌβπ§) β βπ§(π§ β π΅ β§ π¦ = (πΌβπ§))) |
35 | 33, 34 | bitri 275 |
. . . . . . . . . 10
β’
(βπ§ β
π΅ (πΌβπ§) = π¦ β βπ§(π§ β π΅ β§ π¦ = (πΌβπ§))) |
36 | 31, 35 | bitrdi 287 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β π) β§ π β π¦) β (π¦ β ran πΌ β βπ§(π§ β π΅ β§ π¦ = (πΌβπ§)))) |
37 | 36 | ex 414 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β π¦ β (π¦ β ran πΌ β βπ§(π§ β π΅ β§ π¦ = (πΌβπ§))))) |
38 | 37 | pm5.32rd 579 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((π¦ β ran πΌ β§ π β π¦) β (βπ§(π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦))) |
39 | | df-rex 3075 |
. . . . . . . 8
β’
(βπ§ β
{π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§) β βπ§(π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} β§ π¦ = (πΌβπ§))) |
40 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β (πΌβπ₯) = (πΌβπ§)) |
41 | 40 | sseq2d 3981 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (π β (πΌβπ₯) β π β (πΌβπ§))) |
42 | 41 | elrab 3650 |
. . . . . . . . . . 11
β’ (π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} β (π§ β π΅ β§ π β (πΌβπ§))) |
43 | 42 | anbi1i 625 |
. . . . . . . . . 10
β’ ((π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} β§ π¦ = (πΌβπ§)) β ((π§ β π΅ β§ π β (πΌβπ§)) β§ π¦ = (πΌβπ§))) |
44 | | sseq2 3975 |
. . . . . . . . . . . 12
β’ (π¦ = (πΌβπ§) β (π β π¦ β π β (πΌβπ§))) |
45 | 44 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π¦ = (πΌβπ§) β ((π§ β π΅ β§ π β π¦) β (π§ β π΅ β§ π β (πΌβπ§)))) |
46 | 45 | pm5.32ri 577 |
. . . . . . . . . 10
β’ (((π§ β π΅ β§ π β π¦) β§ π¦ = (πΌβπ§)) β ((π§ β π΅ β§ π β (πΌβπ§)) β§ π¦ = (πΌβπ§))) |
47 | | an32 645 |
. . . . . . . . . 10
β’ (((π§ β π΅ β§ π β π¦) β§ π¦ = (πΌβπ§)) β ((π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦)) |
48 | 43, 46, 47 | 3bitr2i 299 |
. . . . . . . . 9
β’ ((π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} β§ π¦ = (πΌβπ§)) β ((π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦)) |
49 | 48 | exbii 1851 |
. . . . . . . 8
β’
(βπ§(π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} β§ π¦ = (πΌβπ§)) β βπ§((π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦)) |
50 | | 19.41v 1954 |
. . . . . . . 8
β’
(βπ§((π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦) β (βπ§(π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦)) |
51 | 39, 49, 50 | 3bitrri 298 |
. . . . . . 7
β’
((βπ§(π§ β π΅ β§ π¦ = (πΌβπ§)) β§ π β π¦) β βπ§ β {π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§)) |
52 | 38, 51 | bitr2di 288 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β (βπ§ β {π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§) β (π¦ β ran πΌ β§ π β π¦))) |
53 | 52 | abbidv 2806 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β {π¦ β£ βπ§ β {π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§)} = {π¦ β£ (π¦ β ran πΌ β§ π β π¦)}) |
54 | | df-rab 3411 |
. . . . 5
β’ {π¦ β ran πΌ β£ π β π¦} = {π¦ β£ (π¦ β ran πΌ β§ π β π¦)} |
55 | 53, 54 | eqtr4di 2795 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β {π¦ β£ βπ§ β {π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§)} = {π¦ β ran πΌ β£ π β π¦}) |
56 | 55 | inteqd 4917 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β β© {π¦ β£ βπ§ β {π₯ β π΅ β£ π β (πΌβπ₯)}π¦ = (πΌβπ§)} = β© {π¦ β ran πΌ β£ π β π¦}) |
57 | 27, 56 | eqtrid 2789 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β β©
π§ β {π₯ β π΅ β£ π β (πΌβπ₯)} (πΌβπ§) = β© {π¦ β ran πΌ β£ π β π¦}) |
58 | 25, 57 | eqtrd 2777 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(πΊβ{π₯ β π΅ β£ π β (πΌβπ₯)})) = β© {π¦ β ran πΌ β£ π β π¦}) |