Metamath Proof Explorer

Theorem dihoml4c

Description: Version of dihoml4 with closed subspaces. (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dihoml4c.h 
|- H = ( LHyp ` K )
dihoml4c.i 
|- I = ( ( DIsoH ` K ) ` W )
dihoml4c.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dihoml4c.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihoml4c.x 
|- ( ph -> X e. ran I )
dihoml4c.y 
|- ( ph -> Y e. ran I )
dihoml4c.l 
|- ( ph -> X C_ Y )
Assertion dihoml4c 
|- ( ph -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = X )

Proof

Step Hyp Ref Expression
1 dihoml4c.h 
 |-  H = ( LHyp ` K )
2 dihoml4c.i 
 |-  I = ( ( DIsoH ` K ) ` W )
3 dihoml4c.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
4 dihoml4c.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
5 dihoml4c.x 
 |-  ( ph -> X e. ran I )
6 dihoml4c.y 
 |-  ( ph -> Y e. ran I )
7 dihoml4c.l 
 |-  ( ph -> X C_ Y )
8 eqid 
 |-  ( meet ` K ) = ( meet ` K )
9 inss1 
 |-  ( ( ._|_ ` X ) i^i Y ) C_ ( ._|_ ` X )
10 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
11 eqid 
 |-  ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
12 1 10 2 11 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
13 4 5 12 syl2anc 
 |-  ( ph -> X C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
14 1 10 11 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( ._|_ ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
15 4 13 14 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
16 9 15 sstrid 
 |-  ( ph -> ( ( ._|_ ` X ) i^i Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
17 1 2 10 11 3 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` X ) i^i Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) e. ran I )
18 4 16 17 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) e. ran I )
19 8 1 2 4 18 6 dihmeet2 
 |-  ( ph -> ( `' I ` ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) ) = ( ( `' I ` ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) ) ( meet ` K ) ( `' I ` Y ) ) )
20 eqid 
 |-  ( oc ` K ) = ( oc ` K )
21 1 2 10 11 3 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( ._|_ ` X ) e. ran I )
22 4 13 21 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. ran I )
23 1 2 dihmeetcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` X ) e. ran I /\ Y e. ran I ) ) -> ( ( ._|_ ` X ) i^i Y ) e. ran I )
24 4 22 6 23 syl12anc 
 |-  ( ph -> ( ( ._|_ ` X ) i^i Y ) e. ran I )
25 20 1 2 3 4 24 dochvalr3 
 |-  ( ph -> ( ( oc ` K ) ` ( `' I ` ( ( ._|_ ` X ) i^i Y ) ) ) = ( `' I ` ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) ) )
26 8 1 2 4 22 6 dihmeet2 
 |-  ( ph -> ( `' I ` ( ( ._|_ ` X ) i^i Y ) ) = ( ( `' I ` ( ._|_ ` X ) ) ( meet ` K ) ( `' I ` Y ) ) )
27 20 1 2 3 4 5 dochvalr3 
 |-  ( ph -> ( ( oc ` K ) ` ( `' I ` X ) ) = ( `' I ` ( ._|_ ` X ) ) )
28 27 oveq1d 
 |-  ( ph -> ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) = ( ( `' I ` ( ._|_ ` X ) ) ( meet ` K ) ( `' I ` Y ) ) )
29 26 28 eqtr4d 
 |-  ( ph -> ( `' I ` ( ( ._|_ ` X ) i^i Y ) ) = ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) )
30 29 fveq2d 
 |-  ( ph -> ( ( oc ` K ) ` ( `' I ` ( ( ._|_ ` X ) i^i Y ) ) ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) ) )
31 25 30 eqtr3d 
 |-  ( ph -> ( `' I ` ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) ) )
32 31 oveq1d 
 |-  ( ph -> ( ( `' I ` ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) ) ( meet ` K ) ( `' I ` Y ) ) = ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) ) ( meet ` K ) ( `' I ` Y ) ) )
33 eqid 
 |-  ( le ` K ) = ( le ` K )
34 33 1 2 4 5 6 dihcnvord 
 |-  ( ph -> ( ( `' I ` X ) ( le ` K ) ( `' I ` Y ) <-> X C_ Y ) )
35 7 34 mpbird 
 |-  ( ph -> ( `' I ` X ) ( le ` K ) ( `' I ` Y ) )
36 4 simpld 
 |-  ( ph -> K e. HL )
37 hloml 
 |-  ( K e. HL -> K e. OML )
38 36 37 syl 
 |-  ( ph -> K e. OML )
39 eqid 
 |-  ( Base ` K ) = ( Base ` K )
40 39 1 2 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
41 4 5 40 syl2anc 
 |-  ( ph -> ( `' I ` X ) e. ( Base ` K ) )
42 39 1 2 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( `' I ` Y ) e. ( Base ` K ) )
43 4 6 42 syl2anc 
 |-  ( ph -> ( `' I ` Y ) e. ( Base ` K ) )
44 39 33 8 20 omllaw4 
 |-  ( ( K e. OML /\ ( `' I ` X ) e. ( Base ` K ) /\ ( `' I ` Y ) e. ( Base ` K ) ) -> ( ( `' I ` X ) ( le ` K ) ( `' I ` Y ) -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) ) ( meet ` K ) ( `' I ` Y ) ) = ( `' I ` X ) ) )
45 38 41 43 44 syl3anc 
 |-  ( ph -> ( ( `' I ` X ) ( le ` K ) ( `' I ` Y ) -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) ) ( meet ` K ) ( `' I ` Y ) ) = ( `' I ` X ) ) )
46 35 45 mpd 
 |-  ( ph -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( `' I ` X ) ) ( meet ` K ) ( `' I ` Y ) ) ) ( meet ` K ) ( `' I ` Y ) ) = ( `' I ` X ) )
47 19 32 46 3eqtrd 
 |-  ( ph -> ( `' I ` ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) ) = ( `' I ` X ) )
48 1 2 dihmeetcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) e. ran I /\ Y e. ran I ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) e. ran I )
49 4 18 6 48 syl12anc 
 |-  ( ph -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) e. ran I )
50 1 2 4 49 5 dihcnv11 
 |-  ( ph -> ( ( `' I ` ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) ) = ( `' I ` X ) <-> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = X ) )
51 47 50 mpbid 
 |-  ( ph -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = X )