Metamath Proof Explorer

Theorem dochoc

Description: Double negative law for orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dochoc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochoc.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochoc.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochoc ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dochoc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochoc.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dochoc.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
5 4 1 2 3 dochvalr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ 𝑋 ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
6 5 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) )
7 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 7 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝐾 ∈ OP )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 1 2 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
11 9 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
12 8 10 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
13 9 1 2 dihcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ∈ ran 𝐼 )
14 12 13 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ∈ ran 𝐼 )
15 4 1 2 3 dochvalr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ∈ ran 𝐼 ) → ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) ) ) )
16 14 15 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) ) ) )
17 9 1 2 dihcnvid1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
18 12 17 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
19 18 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
20 9 4 opococ ⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) = ( ◡ 𝐼 ‘ 𝑋 ) )
21 8 10 20 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) = ( ◡ 𝐼 ‘ 𝑋 ) )
22 19 21 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) ) = ( ◡ 𝐼 ‘ 𝑋 ) )
23 22 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
24 1 2 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
25 23 24 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) ) ) = 𝑋 )
26 16 25 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) ) = 𝑋 )
27 6 26 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )