Metamath Proof Explorer


Theorem dihoml4c

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

Ref Expression
Hypotheses dihoml4c.h 𝐻 = ( LHyp ‘ 𝐾 )
dihoml4c.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihoml4c.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dihoml4c.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dihoml4c.x ( 𝜑𝑋 ∈ ran 𝐼 )
dihoml4c.y ( 𝜑𝑌 ∈ ran 𝐼 )
dihoml4c.l ( 𝜑𝑋𝑌 )
Assertion dihoml4c ( 𝜑 → ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dihoml4c.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dihoml4c.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dihoml4c.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 dihoml4c.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
5 dihoml4c.x ( 𝜑𝑋 ∈ ran 𝐼 )
6 dihoml4c.y ( 𝜑𝑌 ∈ ran 𝐼 )
7 dihoml4c.l ( 𝜑𝑋𝑌 )
8 eqid ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
9 inss1 ( ( 𝑋 ) ∩ 𝑌 ) ⊆ ( 𝑋 )
10 eqid ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
12 1 10 2 11 dihrnss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
13 4 5 12 syl2anc ( 𝜑𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 1 10 11 3 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
15 4 13 14 syl2anc ( 𝜑 → ( 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
16 9 15 sstrid ( 𝜑 → ( ( 𝑋 ) ∩ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
17 1 2 10 11 3 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑋 ) ∩ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∈ ran 𝐼 )
18 4 16 17 syl2anc ( 𝜑 → ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∈ ran 𝐼 )
19 8 1 2 4 18 6 dihmeet2 ( 𝜑 → ( 𝐼 ‘ ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ) = ( ( 𝐼 ‘ ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) )
20 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
21 1 2 10 11 3 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑋 ) ∈ ran 𝐼 )
22 4 13 21 syl2anc ( 𝜑 → ( 𝑋 ) ∈ ran 𝐼 )
23 1 2 dihmeetcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑋 ) ∈ ran 𝐼𝑌 ∈ ran 𝐼 ) ) → ( ( 𝑋 ) ∩ 𝑌 ) ∈ ran 𝐼 )
24 4 22 6 23 syl12anc ( 𝜑 → ( ( 𝑋 ) ∩ 𝑌 ) ∈ ran 𝐼 )
25 20 1 2 3 4 24 dochvalr3 ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ) = ( 𝐼 ‘ ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ) )
26 8 1 2 4 22 6 dihmeet2 ( 𝜑 → ( 𝐼 ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) )
27 20 1 2 3 4 5 dochvalr3 ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑋 ) ) )
28 27 oveq1d ( 𝜑 → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) )
29 26 28 eqtr4d ( 𝜑 → ( 𝐼 ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) )
30 29 fveq2d ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) ) )
31 25 30 eqtr3d ( 𝜑 → ( 𝐼 ‘ ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) ) )
32 31 oveq1d ( 𝜑 → ( ( 𝐼 ‘ ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) )
33 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
34 33 1 2 4 5 6 dihcnvord ( 𝜑 → ( ( 𝐼𝑋 ) ( le ‘ 𝐾 ) ( 𝐼𝑌 ) ↔ 𝑋𝑌 ) )
35 7 34 mpbird ( 𝜑 → ( 𝐼𝑋 ) ( le ‘ 𝐾 ) ( 𝐼𝑌 ) )
36 4 simpld ( 𝜑𝐾 ∈ HL )
37 hloml ( 𝐾 ∈ HL → 𝐾 ∈ OML )
38 36 37 syl ( 𝜑𝐾 ∈ OML )
39 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
40 39 1 2 dihcnvcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼𝑋 ) ∈ ( Base ‘ 𝐾 ) )
41 4 5 40 syl2anc ( 𝜑 → ( 𝐼𝑋 ) ∈ ( Base ‘ 𝐾 ) )
42 39 1 2 dihcnvcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼𝑌 ) ∈ ( Base ‘ 𝐾 ) )
43 4 6 42 syl2anc ( 𝜑 → ( 𝐼𝑌 ) ∈ ( Base ‘ 𝐾 ) )
44 39 33 8 20 omllaw4 ( ( 𝐾 ∈ OML ∧ ( 𝐼𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐼𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼𝑋 ) ( le ‘ 𝐾 ) ( 𝐼𝑌 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) = ( 𝐼𝑋 ) ) )
45 38 41 43 44 syl3anc ( 𝜑 → ( ( 𝐼𝑋 ) ( le ‘ 𝐾 ) ( 𝐼𝑌 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) = ( 𝐼𝑋 ) ) )
46 35 45 mpd ( 𝜑 → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝐼𝑋 ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) ) ( meet ‘ 𝐾 ) ( 𝐼𝑌 ) ) = ( 𝐼𝑋 ) )
47 19 32 46 3eqtrd ( 𝜑 → ( 𝐼 ‘ ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ) = ( 𝐼𝑋 ) )
48 1 2 dihmeetcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∈ ran 𝐼𝑌 ∈ ran 𝐼 ) ) → ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ∈ ran 𝐼 )
49 4 18 6 48 syl12anc ( 𝜑 → ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ∈ ran 𝐼 )
50 1 2 4 49 5 dihcnv11 ( 𝜑 → ( ( 𝐼 ‘ ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ) = ( 𝐼𝑋 ) ↔ ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 ) )
51 47 50 mpbid ( 𝜑 → ( ( ‘ ( ( 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 )