Theorem dochvalr2

Description: Orthocomplement of a closed subspace. (Contributed by NM, 21-Jul-2014)

	Ref	Expression
Hypotheses	dochvalr2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dochvalr2.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	dochvalr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochvalr2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dochvalr2.n	⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dochvalr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochvalr2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dochvalr2.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3		dochvalr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dochvalr2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5		dochvalr2.n	⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6	1 3 4	dihcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 )
7	2 3 4 5	dochvalr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) ) )
8	6 7	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) ) )
9	1 3 4	dihcnvid1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 )
10	9	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
11	10	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) ) = ( 𝐼 ‘ ( ⊥ ‘ 𝑋 ) ) )
12	8 11	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ⊥ ‘ 𝑋 ) ) )