Theorem hlhilocv

Description: The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

	Ref	Expression
Hypotheses	hlhil0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hlhil0.l	⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hlhil0.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
	hlhil0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hlhilocv.v	⊢ 𝑉 = ( Base ‘ 𝐿 )
	hlhilocv.n	⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hlhilocv.o	⊢ 𝑂 = ( ocv ‘ 𝑈 )
	hlhilocv.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion	hlhilocv	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		hlhil0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hlhil0.l	⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hlhil0.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
4		hlhil0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5		hlhilocv.v	⊢ 𝑉 = ( Base ‘ 𝐿 )
6		hlhilocv.n	⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7		hlhilocv.o	⊢ 𝑂 = ( ocv ‘ 𝑈 )
8		hlhilocv.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
9	1 3 4 2 5	hlhilbase	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑈 ) )
10		rabeq	⊢ ( 𝑉 = ( Base ‘ 𝑈 ) → { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } = { 𝑦 ∈ ( Base ‘ 𝑈 ) ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } )
11	9 10	syl	⊢ ( 𝜑 → { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } = { 𝑦 ∈ ( Base ‘ 𝑈 ) ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } )
12		eqid	⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
13	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		eqid	⊢ ( ·𝑖 ‘ 𝑈 ) = ( ·𝑖 ‘ 𝑈 )
15		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑦 ∈ 𝑉 )
16	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → 𝑋 ⊆ 𝑉 )
17	16	sselda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑉 )
18	1 2 5 12 3 13 14 15 17	hlhilipval	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑧 ) ‘ 𝑦 ) )
19		eqid	⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
20		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
21		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐿 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) )
22	1 2 19 3 20 4 21	hlhils0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐿 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
23	22	eqcomd	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
24	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
25	18 24	eqeq12d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ↔ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑧 ) ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) ) )
26	25	ralbidva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑧 ) ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) ) )
27	26	rabbidva	⊢ ( 𝜑 → { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑧 ) ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } )
28	11 27	eqtr3d	⊢ ( 𝜑 → { 𝑦 ∈ ( Base ‘ 𝑈 ) ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑧 ) ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } )
29	8 9	sseqtrd	⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
30		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
31		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
32	30 14 20 31 7	ocvval	⊢ ( 𝑋 ⊆ ( Base ‘ 𝑈 ) → ( 𝑂 ‘ 𝑋 ) = { 𝑦 ∈ ( Base ‘ 𝑈 ) ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } )
33	29 32	syl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = { 𝑦 ∈ ( Base ‘ 𝑈 ) ∣ ∀ 𝑧 ∈ 𝑋 ( 𝑦 ( ·𝑖 ‘ 𝑈 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } )
34	1 2 5 19 21 6 12 4 8	hdmapoc	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑧 ) ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } )
35	28 33 34	3eqtr4d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )