Metamath Proof Explorer

Theorem hdmapoc

Description: Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in Holland95 p. 14. (Contributed by NM, 17-Jun-2015)

Ref Expression
Hypotheses hdmapoc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapoc.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapoc.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapoc.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapoc.z ⊢ 0 = ( 0g ‘ 𝑅 )
hdmapoc.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hdmapoc.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapoc.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapoc.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion hdmapoc ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 } )

Proof

Step Hyp Ref Expression
1 hdmapoc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapoc.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapoc.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmapoc.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5 hdmapoc.z ⊢ 0 = ( 0g ‘ 𝑅 )
6 hdmapoc.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7 hdmapoc.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8 hdmapoc.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 hdmapoc.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
10 1 2 3 6 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑂 ‘ 𝑋 ) ⊆ 𝑉 )
11 8 9 10 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ⊆ 𝑉 )
12 11 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) → 𝑦 ∈ 𝑉 ) )
13 12 pm4.71rd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ) ) )
14 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
15 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
16 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → 𝑈 ∈ LMod )
18 1 2 3 14 6 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑂 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
19 8 9 18 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑂 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 )
22 3 14 15 17 20 21 lspsnel5 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ↔ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ⊆ ( 𝑂 ‘ 𝑋 ) ) )
23 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
25 1 2 3 15 23 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 24 21 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 1 23 2 3 6 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑂 ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
28 8 9 27 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑂 ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
30 1 23 6 24 26 29 dochord ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ⊆ ( 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ( 𝑂 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ) ) )
31 21 snssd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → { 𝑦 } ⊆ 𝑉 )
32 1 2 6 3 15 24 31 dochocsp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑂 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ) = ( 𝑂 ‘ { 𝑦 } ) )
33 32 sseq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑂 ‘ ( 𝑂 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ) ↔ ( 𝑂 ‘ ( 𝑂 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ { 𝑦 } ) ) )
34 9 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → 𝑋 ⊆ 𝑉 )
35 1 23 2 3 6 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑦 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝑦 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
36 24 31 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑂 ‘ { 𝑦 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
37 1 2 3 23 6 24 34 36 dochsscl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑋 ⊆ ( 𝑂 ‘ { 𝑦 } ) ↔ ( 𝑂 ‘ ( 𝑂 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ { 𝑦 } ) ) )
38 33 37 bitr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑂 ‘ ( 𝑂 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑦 } ) ) ↔ 𝑋 ⊆ ( 𝑂 ‘ { 𝑦 } ) ) )
39 22 30 38 3bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ↔ 𝑋 ⊆ ( 𝑂 ‘ { 𝑦 } ) ) )
40 dfss3 ⊢ ( 𝑋 ⊆ ( 𝑂 ‘ { 𝑦 } ) ↔ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ ( 𝑂 ‘ { 𝑦 } ) )
41 39 40 bitrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ ( 𝑂 ‘ { 𝑦 } ) ) )
42 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
43 34 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑉 )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑦 ∈ 𝑉 )
45 1 6 2 3 4 5 7 42 43 44 hdmapellkr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ↔ 𝑦 ∈ ( 𝑂 ‘ { 𝑧 } ) ) )
46 1 6 2 3 42 44 43 dochsncom ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ∈ ( 𝑂 ‘ { 𝑧 } ) ↔ 𝑧 ∈ ( 𝑂 ‘ { 𝑦 } ) ) )
47 45 46 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ↔ 𝑧 ∈ ( 𝑂 ‘ { 𝑦 } ) ) )
48 47 ralbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ↔ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ ( 𝑂 ‘ { 𝑦 } ) ) )
49 41 48 bitr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ) )
50 49 pm5.32da ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ) ) )
51 13 50 bitrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑂 ‘ 𝑋 ) ↔ ( 𝑦 ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ) ) )
52 51 eqabdv ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ) } )
53 df-rab ⊢ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 } = { 𝑦 ∣ ( 𝑦 ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 ) }
54 52 53 eqtr4di ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑆 ‘ 𝑧 ) ‘ 𝑦 ) = 0 } )