Metamath Proof Explorer


Theorem dochcl

Description: Closure of subspace orthocomplement for DVecH vector space. (Contributed by NM, 9-Mar-2014)

Ref Expression
Hypotheses dochcl.h 𝐻 = ( LHyp ‘ 𝐾 )
dochcl.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochcl.v 𝑉 = ( Base ‘ 𝑈 )
dochcl.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dochcl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochcl.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dochcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochcl.v 𝑉 = ( Base ‘ 𝑈 )
5 dochcl.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
8 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 6 7 8 1 2 3 4 5 dochval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ) ) )
10 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
11 10 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝐾 ∈ OP )
12 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
13 12 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝐾 ∈ CLat )
14 ssrab2 { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ⊆ ( Base ‘ 𝐾 )
15 6 7 clatglbcl ( ( 𝐾 ∈ CLat ∧ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ⊆ ( Base ‘ 𝐾 ) ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ∈ ( Base ‘ 𝐾 ) )
16 13 14 15 sylancl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ∈ ( Base ‘ 𝐾 ) )
17 6 8 opoccl ( ( 𝐾 ∈ OP ∧ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ) ∈ ( Base ‘ 𝐾 ) )
18 11 16 17 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ) ∈ ( Base ‘ 𝐾 ) )
19 6 1 2 dihcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ) ) ∈ ran 𝐼 )
20 18 19 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼𝑦 ) } ) ) ) ∈ ran 𝐼 )
21 9 20 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ ran 𝐼 )