Metamath Proof Explorer


Theorem dochsatshpb

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochsatshpb.h 𝐻 = ( LHyp ‘ 𝐾 )
dochsatshpb.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsatshpb.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsatshpb.s 𝑆 = ( LSubSp ‘ 𝑈 )
dochsatshpb.a 𝐴 = ( LSAtoms ‘ 𝑈 )
dochsatshpb.y 𝑌 = ( LSHyp ‘ 𝑈 )
dochsatshpb.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochsatshpb.q ( 𝜑𝑄𝑆 )
Assertion dochsatshpb ( 𝜑 → ( 𝑄𝐴 ↔ ( 𝑄 ) ∈ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dochsatshpb.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsatshpb.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsatshpb.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsatshpb.s 𝑆 = ( LSubSp ‘ 𝑈 )
5 dochsatshpb.a 𝐴 = ( LSAtoms ‘ 𝑈 )
6 dochsatshpb.y 𝑌 = ( LSHyp ‘ 𝑈 )
7 dochsatshpb.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 dochsatshpb.q ( 𝜑𝑄𝑆 )
9 7 adantr ( ( 𝜑𝑄𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 simpr ( ( 𝜑𝑄𝐴 ) → 𝑄𝐴 )
11 1 3 2 5 6 9 10 dochsatshp ( ( 𝜑𝑄𝐴 ) → ( 𝑄 ) ∈ 𝑌 )
12 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
13 12 4 lssss ( 𝑄𝑆𝑄 ⊆ ( Base ‘ 𝑈 ) )
14 8 13 syl ( 𝜑𝑄 ⊆ ( Base ‘ 𝑈 ) )
15 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
16 1 15 3 12 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
17 7 14 16 syl2anc ( 𝜑 → ( 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
18 1 15 2 dochoc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ‘ ( ‘ ( 𝑄 ) ) ) = ( 𝑄 ) )
19 7 17 18 syl2anc ( 𝜑 → ( ‘ ( ‘ ( 𝑄 ) ) ) = ( 𝑄 ) )
20 19 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ‘ ( ‘ ( 𝑄 ) ) ) = ( 𝑄 ) )
21 1 3 7 dvhlmod ( 𝜑𝑈 ∈ LMod )
22 21 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → 𝑈 ∈ LMod )
23 simpr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( 𝑄 ) ∈ 𝑌 )
24 12 6 22 23 lshpne ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( 𝑄 ) ≠ ( Base ‘ 𝑈 ) )
25 20 24 eqnetrd ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ‘ ( ‘ ( 𝑄 ) ) ) ≠ ( Base ‘ 𝑈 ) )
26 eqid ( 0g𝑈 ) = ( 0g𝑈 )
27 1 3 12 2 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
28 7 14 27 syl2anc ( 𝜑 → ( 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
29 1 2 3 12 26 7 28 dochn0nv ( 𝜑 → ( ( ‘ ( 𝑄 ) ) ≠ { ( 0g𝑈 ) } ↔ ( ‘ ( ‘ ( 𝑄 ) ) ) ≠ ( Base ‘ 𝑈 ) ) )
30 29 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ( ‘ ( 𝑄 ) ) ≠ { ( 0g𝑈 ) } ↔ ( ‘ ( ‘ ( 𝑄 ) ) ) ≠ ( Base ‘ 𝑈 ) ) )
31 25 30 mpbird ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ‘ ( 𝑄 ) ) ≠ { ( 0g𝑈 ) } )
32 1 3 12 4 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑄 ) ∈ 𝑆 )
33 7 14 32 syl2anc ( 𝜑 → ( 𝑄 ) ∈ 𝑆 )
34 12 4 lssss ( ( 𝑄 ) ∈ 𝑆 → ( 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
35 33 34 syl ( 𝜑 → ( 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
36 1 3 12 4 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ‘ ( 𝑄 ) ) ∈ 𝑆 )
37 7 35 36 syl2anc ( 𝜑 → ( ‘ ( 𝑄 ) ) ∈ 𝑆 )
38 37 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ‘ ( 𝑄 ) ) ∈ 𝑆 )
39 26 4 lssne0 ( ( ‘ ( 𝑄 ) ) ∈ 𝑆 → ( ( ‘ ( 𝑄 ) ) ≠ { ( 0g𝑈 ) } ↔ ∃ 𝑣 ∈ ( ‘ ( 𝑄 ) ) 𝑣 ≠ ( 0g𝑈 ) ) )
40 38 39 syl ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ( ‘ ( 𝑄 ) ) ≠ { ( 0g𝑈 ) } ↔ ∃ 𝑣 ∈ ( ‘ ( 𝑄 ) ) 𝑣 ≠ ( 0g𝑈 ) ) )
41 31 40 mpbid ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ∃ 𝑣 ∈ ( ‘ ( 𝑄 ) ) 𝑣 ≠ ( 0g𝑈 ) )
42 7 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
43 42 3ad2ant1 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
44 17 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
45 44 3ad2ant1 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
46 43 45 18 syl2anc ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( ‘ ( 𝑄 ) ) ) = ( 𝑄 ) )
47 eqid ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
48 22 3ad2ant1 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → 𝑈 ∈ LMod )
49 38 3ad2ant1 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( 𝑄 ) ) ∈ 𝑆 )
50 simp2 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → 𝑣 ∈ ( ‘ ( 𝑄 ) ) )
51 4 47 48 49 50 lspsnel5a ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ⊆ ( ‘ ( 𝑄 ) ) )
52 12 4 lssel ( ( ( ‘ ( 𝑄 ) ) ∈ 𝑆𝑣 ∈ ( ‘ ( 𝑄 ) ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
53 49 50 52 syl2anc ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
54 1 3 12 47 15 dihlsprn ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
55 43 53 54 syl2anc ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
56 1 15 3 12 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ‘ ( 𝑄 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
57 7 35 56 syl2anc ( 𝜑 → ( ‘ ( 𝑄 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
58 57 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ‘ ( 𝑄 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
59 58 3ad2ant1 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( 𝑄 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
60 1 15 2 43 55 59 dochord ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ⊆ ( ‘ ( 𝑄 ) ) ↔ ( ‘ ( ‘ ( 𝑄 ) ) ) ⊆ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
61 51 60 mpbid ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( ‘ ( 𝑄 ) ) ) ⊆ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
62 46 61 eqsstrrd ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( 𝑄 ) ⊆ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
63 1 3 7 dvhlvec ( 𝜑𝑈 ∈ LVec )
64 63 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → 𝑈 ∈ LVec )
65 64 3ad2ant1 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → 𝑈 ∈ LVec )
66 simp1r ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( 𝑄 ) ∈ 𝑌 )
67 simp3 ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → 𝑣 ≠ ( 0g𝑈 ) )
68 12 47 26 5 lsatlspsn2 ( ( 𝑈 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ∈ 𝐴 )
69 48 53 67 68 syl3anc ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ∈ 𝐴 )
70 1 3 2 5 6 43 69 dochsatshp ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ∈ 𝑌 )
71 6 65 66 70 lshpcmp ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ( 𝑄 ) ⊆ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( 𝑄 ) = ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
72 62 71 mpbid ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( 𝑄 ) = ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
73 72 fveq2d ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( 𝑄 ) ) = ( ‘ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
74 1 15 2 dochoc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ‘ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
75 43 55 74 syl2anc ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
76 73 75 eqtrd ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( 𝑄 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
77 76 69 eqeltrd ( ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ‘ ( 𝑄 ) ) ∧ 𝑣 ≠ ( 0g𝑈 ) ) → ( ‘ ( 𝑄 ) ) ∈ 𝐴 )
78 77 rexlimdv3a ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ∃ 𝑣 ∈ ( ‘ ( 𝑄 ) ) 𝑣 ≠ ( 0g𝑈 ) → ( ‘ ( 𝑄 ) ) ∈ 𝐴 ) )
79 41 78 mpd ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ‘ ( 𝑄 ) ) ∈ 𝐴 )
80 8 adantr ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → 𝑄𝑆 )
81 1 2 3 4 5 42 80 dochsat ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → ( ( ‘ ( 𝑄 ) ) ∈ 𝐴𝑄𝐴 ) )
82 79 81 mpbid ( ( 𝜑 ∧ ( 𝑄 ) ∈ 𝑌 ) → 𝑄𝐴 )
83 11 82 impbida ( 𝜑 → ( 𝑄𝐴 ↔ ( 𝑄 ) ∈ 𝑌 ) )