Step | Hyp | Ref
| Expression |
1 | | hlhillcs.u |
. . . . . . 7
β’ π = ((HLHilβπΎ)βπ) |
2 | 1 | fvexi 6861 |
. . . . . 6
β’ π β V |
3 | | eqid 2737 |
. . . . . . 7
β’
(ocvβπ) =
(ocvβπ) |
4 | | hlhillcs.c |
. . . . . . 7
β’ πΆ = (ClSubSpβπ) |
5 | 3, 4 | iscss 21103 |
. . . . . 6
β’ (π β V β (π₯ β πΆ β π₯ = ((ocvβπ)β((ocvβπ)βπ₯)))) |
6 | 2, 5 | mp1i 13 |
. . . . 5
β’ (π β (π₯ β πΆ β π₯ = ((ocvβπ)β((ocvβπ)βπ₯)))) |
7 | 6 | biimpa 478 |
. . . 4
β’ ((π β§ π₯ β πΆ) β π₯ = ((ocvβπ)β((ocvβπ)βπ₯))) |
8 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
9 | 8, 4 | cssss 21105 |
. . . . 5
β’ (π₯ β πΆ β π₯ β (Baseβπ)) |
10 | | hlhillcs.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
11 | | hlhillcs.i |
. . . . . . 7
β’ πΌ = ((DIsoHβπΎ)βπ) |
12 | | eqid 2737 |
. . . . . . 7
β’
((DVecHβπΎ)βπ) = ((DVecHβπΎ)βπ) |
13 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ((DVecHβπΎ)βπ)) = (Baseβ((DVecHβπΎ)βπ)) |
14 | | eqid 2737 |
. . . . . . 7
β’
((ocHβπΎ)βπ) = ((ocHβπΎ)βπ) |
15 | | hlhillcs.k |
. . . . . . . 8
β’ (π β (πΎ β HL β§ π β π»)) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β (πΎ β HL β§ π β π»)) |
17 | 10, 1, 15, 12, 13 | hlhilbase 40428 |
. . . . . . . . 9
β’ (π β
(Baseβ((DVecHβπΎ)βπ)) = (Baseβπ)) |
18 | 17 | sseq2d 3981 |
. . . . . . . 8
β’ (π β (π₯ β (Baseβ((DVecHβπΎ)βπ)) β π₯ β (Baseβπ))) |
19 | 18 | biimpar 479 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β π₯ β (Baseβ((DVecHβπΎ)βπ))) |
20 | 10, 11, 12, 13, 14, 16, 19 | dochoccl 39861 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (π₯ β ran πΌ β (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯)) |
21 | | eqcom 2744 |
. . . . . . 7
β’ (π₯ = ((ocvβπ)β((ocvβπ)βπ₯)) β ((ocvβπ)β((ocvβπ)βπ₯)) = π₯) |
22 | 10, 12, 1, 16, 13, 14, 3, 19 | hlhilocv 40453 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β ((ocvβπ)βπ₯) = (((ocHβπΎ)βπ)βπ₯)) |
23 | 22 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β ((ocvβπ)β((ocvβπ)βπ₯)) = ((ocvβπ)β(((ocHβπΎ)βπ)βπ₯))) |
24 | 10, 12, 13, 14 | dochssv 39847 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π₯ β (Baseβ((DVecHβπΎ)βπ))) β (((ocHβπΎ)βπ)βπ₯) β (Baseβ((DVecHβπΎ)βπ))) |
25 | 16, 19, 24 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (((ocHβπΎ)βπ)βπ₯) β (Baseβ((DVecHβπΎ)βπ))) |
26 | 10, 12, 1, 16, 13, 14, 3, 25 | hlhilocv 40453 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β ((ocvβπ)β(((ocHβπΎ)βπ)βπ₯)) = (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯))) |
27 | 23, 26 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ)) β ((ocvβπ)β((ocvβπ)βπ₯)) = (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯))) |
28 | 27 | eqeq1d 2739 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β (((ocvβπ)β((ocvβπ)βπ₯)) = π₯ β (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯)) |
29 | 21, 28 | bitrid 283 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (π₯ = ((ocvβπ)β((ocvβπ)βπ₯)) β (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯)) |
30 | 20, 29 | bitr4d 282 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β (π₯ β ran πΌ β π₯ = ((ocvβπ)β((ocvβπ)βπ₯)))) |
31 | 9, 30 | sylan2 594 |
. . . 4
β’ ((π β§ π₯ β πΆ) β (π₯ β ran πΌ β π₯ = ((ocvβπ)β((ocvβπ)βπ₯)))) |
32 | 7, 31 | mpbird 257 |
. . 3
β’ ((π β§ π₯ β πΆ) β π₯ β ran πΌ) |
33 | | simpr 486 |
. . . 4
β’ ((π β§ π₯ β ran πΌ) β π₯ β ran πΌ) |
34 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ran πΌ) β (πΎ β HL β§ π β π»)) |
35 | 10, 12, 11, 13 | dihrnss 39770 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π₯ β ran πΌ) β π₯ β (Baseβ((DVecHβπΎ)βπ))) |
36 | 15, 35 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ran πΌ) β π₯ β (Baseβ((DVecHβπΎ)βπ))) |
37 | 10, 12, 1, 34, 13, 14, 3, 36 | hlhilocv 40453 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ran πΌ) β ((ocvβπ)βπ₯) = (((ocHβπΎ)βπ)βπ₯)) |
38 | 37 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ran πΌ) β ((ocvβπ)β((ocvβπ)βπ₯)) = ((ocvβπ)β(((ocHβπΎ)βπ)βπ₯))) |
39 | 34, 36, 24 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ran πΌ) β (((ocHβπΎ)βπ)βπ₯) β (Baseβ((DVecHβπΎ)βπ))) |
40 | 10, 12, 1, 34, 13, 14, 3, 39 | hlhilocv 40453 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ran πΌ) β ((ocvβπ)β(((ocHβπΎ)βπ)βπ₯)) = (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯))) |
41 | 38, 40 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π₯ β ran πΌ) β ((ocvβπ)β((ocvβπ)βπ₯)) = (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯))) |
42 | 41 | eqeq1d 2739 |
. . . . . . . 8
β’ ((π β§ π₯ β ran πΌ) β (((ocvβπ)β((ocvβπ)βπ₯)) = π₯ β (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯)) |
43 | 42 | biimpar 479 |
. . . . . . 7
β’ (((π β§ π₯ β ran πΌ) β§ (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯) β ((ocvβπ)β((ocvβπ)βπ₯)) = π₯) |
44 | 43 | eqcomd 2743 |
. . . . . 6
β’ (((π β§ π₯ β ran πΌ) β§ (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯) β π₯ = ((ocvβπ)β((ocvβπ)βπ₯))) |
45 | 44 | ex 414 |
. . . . 5
β’ ((π β§ π₯ β ran πΌ) β ((((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯ β π₯ = ((ocvβπ)β((ocvβπ)βπ₯)))) |
46 | 10, 11, 12, 13, 14, 34, 36 | dochoccl 39861 |
. . . . 5
β’ ((π β§ π₯ β ran πΌ) β (π₯ β ran πΌ β (((ocHβπΎ)βπ)β(((ocHβπΎ)βπ)βπ₯)) = π₯)) |
47 | 2, 5 | mp1i 13 |
. . . . 5
β’ ((π β§ π₯ β ran πΌ) β (π₯ β πΆ β π₯ = ((ocvβπ)β((ocvβπ)βπ₯)))) |
48 | 45, 46, 47 | 3imtr4d 294 |
. . . 4
β’ ((π β§ π₯ β ran πΌ) β (π₯ β ran πΌ β π₯ β πΆ)) |
49 | 33, 48 | mpd 15 |
. . 3
β’ ((π β§ π₯ β ran πΌ) β π₯ β πΆ) |
50 | 32, 49 | impbida 800 |
. 2
β’ (π β (π₯ β πΆ β π₯ β ran πΌ)) |
51 | 50 | eqrdv 2735 |
1
β’ (π β πΆ = ran πΌ) |