Metamath Proof Explorer

Theorem dochvalr3

Description: Orthocomplement of a closed subspace. (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochvalr3.o ⊢ ⊥ = ( oc ‘ 𝐾 )
dochvalr3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochvalr3.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochvalr3.n ⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochvalr3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochvalr3.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
Assertion dochvalr3 ( 𝜑 → ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dochvalr3.o ⊢ ⊥ = ( oc ‘ 𝐾 )
2 dochvalr3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dochvalr3.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dochvalr3.n ⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5 dochvalr3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 dochvalr3.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
7 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
9 2 7 3 8 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
10 5 6 9 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
11 2 3 7 8 4 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑁 ‘ 𝑋 ) ∈ ran 𝐼 )
12 5 10 11 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ ran 𝐼 )
13 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( 𝑁 ‘ 𝑋 ) )
14 5 12 13 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( 𝑁 ‘ 𝑋 ) )
15 1 2 3 4 dochvalr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
16 5 6 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
17 14 16 eqtr2d ⊢ ( 𝜑 → ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) )
18 5 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
19 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
20 18 19 syl ⊢ ( 𝜑 → 𝐾 ∈ OP )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
23 5 6 22 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
24 21 1 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
25 20 23 24 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
26 21 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
27 5 12 26 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
28 21 2 3 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) ↔ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) )
29 5 25 27 28 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) ↔ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) ) )
30 17 29 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( ◡ 𝐼 ‘ ( 𝑁 ‘ 𝑋 ) ) )