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 𝐼 )