Metamath Proof Explorer

Theorem dochvalr

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

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

Proof

Step Hyp Ref Expression
1 dochvalr.o ⊢ ⊥ = ( oc ‘ 𝐾 )
2 dochvalr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dochvalr.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dochvalr.n ⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
7 2 5 3 6 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
10 8 9 1 2 3 5 6 4 dochval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )
11 7 10 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )
12 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
14 13 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝐾 ∈ Lat )
15 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
16 15 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝐾 ∈ CLat )
17 ssrab2 ⊢ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ⊆ ( Base ‘ 𝐾 )
18 8 9 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ⊆ ( Base ‘ 𝐾 ) ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ∈ ( Base ‘ 𝐾 ) )
19 16 17 18 sylancl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ∈ ( Base ‘ 𝐾 ) )
20 8 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
21 17 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ⊆ ( Base ‘ 𝐾 ) )
22 ssid ⊢ 𝑋 ⊆ 𝑋
23 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
24 22 23 sseqtrrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
25 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐼 ‘ 𝑋 ) → ( 𝐼 ‘ 𝑦 ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
26 25 sseq2d ⊢ ( 𝑦 = ( ◡ 𝐼 ‘ 𝑋 ) → ( 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) ↔ 𝑋 ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
27 26 elrab ⊢ ( ( ◡ 𝐼 ‘ 𝑋 ) ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ↔ ( ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
28 20 24 27 sylanbrc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } )
29 8 12 9 clatglble ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ⊆ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑋 ) )
30 16 21 28 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑋 ) )
31 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐼 ‘ 𝑦 ) = ( 𝐼 ‘ 𝑧 ) )
32 31 sseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) ↔ 𝑋 ⊆ ( 𝐼 ‘ 𝑧 ) ) )
33 32 elrab ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ↔ ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ⊆ ( 𝐼 ‘ 𝑧 ) ) )
34 23 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
35 34 sseq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊆ ( 𝐼 ‘ 𝑧 ) ↔ 𝑋 ⊆ ( 𝐼 ‘ 𝑧 ) ) )
36 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
37 20 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
38 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
39 8 12 2 3 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊆ ( 𝐼 ‘ 𝑧 ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
40 36 37 38 39 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊆ ( 𝐼 ‘ 𝑧 ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
41 35 40 bitr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ⊆ ( 𝐼 ‘ 𝑧 ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
42 41 biimpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ⊆ ( 𝐼 ‘ 𝑧 ) → ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
43 42 expimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ⊆ ( 𝐼 ‘ 𝑧 ) ) → ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
44 33 43 syl5bi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝑧 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } → ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
45 44 ralrimiv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ∀ 𝑧 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 )
46 8 12 9 clatleglb ⊢ ( ( 𝐾 ∈ CLat ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ⊆ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ↔ ∀ 𝑧 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
47 16 20 21 46 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ↔ ∀ 𝑧 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) 𝑧 ) )
48 45 47 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) )
49 8 12 14 19 20 30 48 latasymd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) = ( ◡ 𝐼 ‘ 𝑋 ) )
50 49 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) = ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
51 50 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )
52 11 51 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ) )