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 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 )