Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = (πβ{π})) β π = (πβ{π})) |
2 | | dih1dor0.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
3 | | dih1dor0.u |
. . . . . . . 8
β’ π = ((DVecHβπΎ)βπ) |
4 | | dihldor0.v |
. . . . . . . 8
β’ π = (Baseβπ) |
5 | | dih1dor0.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
6 | | dih1dor0.i |
. . . . . . . 8
β’ πΌ = ((DIsoHβπΎ)βπ) |
7 | 2, 3, 4, 5, 6 | dihlsprn 39844 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) |
8 | 7 | 3adant3 1133 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β (πβ{π}) β ran πΌ) |
9 | 8 | ad2antrr 725 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = (πβ{π})) β (πβ{π}) β ran πΌ) |
10 | 1, 9 | eqeltrd 2834 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = (πβ{π})) β π β ran πΌ) |
11 | | simpr 486 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β π = {(0gβπ)}) |
12 | | simpll1 1213 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β (πΎ β HL β§ π β π»)) |
13 | | eqid 2733 |
. . . . . . . 8
β’
(0.βπΎ) =
(0.βπΎ) |
14 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
15 | 13, 2, 6, 3, 14 | dih0 39793 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (πΌβ(0.βπΎ)) = {(0gβπ)}) |
16 | 12, 15 | syl 17 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β (πΌβ(0.βπΎ)) = {(0gβπ)}) |
17 | 11, 16 | eqtr4d 2776 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β π = (πΌβ(0.βπΎ))) |
18 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
19 | 18, 2, 6 | dihfn 39781 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β πΌ Fn (BaseβπΎ)) |
20 | 12, 19 | syl 17 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β πΌ Fn (BaseβπΎ)) |
21 | | simp1l 1198 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β πΎ β HL) |
22 | 21 | ad2antrr 725 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β πΎ β HL) |
23 | | hlop 37874 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OP) |
24 | 18, 13 | op0cl 37696 |
. . . . . . 7
β’ (πΎ β OP β
(0.βπΎ) β
(BaseβπΎ)) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β (0.βπΎ) β (BaseβπΎ)) |
26 | | fnfvelrn 7035 |
. . . . . 6
β’ ((πΌ Fn (BaseβπΎ) β§ (0.βπΎ) β (BaseβπΎ)) β (πΌβ(0.βπΎ)) β ran πΌ) |
27 | 20, 25, 26 | syl2anc 585 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β (πΌβ(0.βπΎ)) β ran πΌ) |
28 | 17, 27 | eqeltrd 2834 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β§ π = {(0gβπ)}) β π β ran πΌ) |
29 | | simpl1 1192 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β (πΎ β HL β§ π β π»)) |
30 | 2, 3, 29 | dvhlvec 39622 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β π β LVec) |
31 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β π β π) |
32 | | simpl2 1193 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β π β π) |
33 | | simpl3 1194 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β π β (πβ{π})) |
34 | | dih1dor0.s |
. . . . . 6
β’ π = (LSubSpβπ) |
35 | 4, 14, 34, 5 | lspsnat 20651 |
. . . . 5
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π = (πβ{π}) β¨ π = {(0gβπ)})) |
36 | 30, 31, 32, 33, 35 | syl31anc 1374 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β (π = (πβ{π}) β¨ π = {(0gβπ)})) |
37 | 10, 28, 36 | mpjaodan 958 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β§ π β π) β π β ran πΌ) |
38 | 37 | ex 414 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β (π β π β π β ran πΌ)) |
39 | 2, 3, 6, 34 | dihsslss 39789 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ran πΌ β π) |
40 | 39 | 3ad2ant1 1134 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β ran πΌ β π) |
41 | 40 | sseld 3947 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β (π β ran πΌ β π β π)) |
42 | 38, 41 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β (π β π β π β ran πΌ)) |