Metamath Proof Explorer

Theorem dochsatshp

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014) (Revised by Mario Carneiro, 1-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 dochsatshp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsatshp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsatshp.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsatshp.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5 dochsatshp.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochsatshp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochsatshp.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
9 1 2 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
10 8 4 9 7 lsatssv ⊢ ( 𝜑 → 𝑄 ⊆ ( Base ‘ 𝑈 ) )
11 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
12 1 2 8 11 3 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
13 6 10 12 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
14 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15 14 4 9 7 lsatn0 ⊢ ( 𝜑 → 𝑄 ≠ { ( 0g ‘ 𝑈 ) } )
16 1 2 3 8 14 doch0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = ( Base ‘ 𝑈 ) )
17 6 16 syl ⊢ ( 𝜑 → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = ( Base ‘ 𝑈 ) )
18 17 eqeq2d ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ↔ ( ⊥ ‘ 𝑄 ) = ( Base ‘ 𝑈 ) ) )
19 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
20 1 2 19 4 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 6 7 20 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
22 1 19 2 14 dih0rn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { ( 0g ‘ 𝑈 ) } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
23 6 22 syl ⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
24 1 19 3 6 21 23 doch11 ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ↔ 𝑄 = { ( 0g ‘ 𝑈 ) } ) )
25 18 24 bitr3d ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) = ( Base ‘ 𝑈 ) ↔ 𝑄 = { ( 0g ‘ 𝑈 ) } ) )
26 25 necon3bid ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) ≠ ( Base ‘ 𝑈 ) ↔ 𝑄 ≠ { ( 0g ‘ 𝑈 ) } ) )
27 15 26 mpbird ⊢ ( 𝜑 → ( ⊥ ‘ 𝑄 ) ≠ ( Base ‘ 𝑈 ) )
28 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
29 8 28 14 4 islsat ⊢ ( 𝑈 ∈ LMod → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
30 9 29 syl ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
31 7 30 mpbid ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
32 eldifi ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
33 32 adantr ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
34 33 a1i ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) ) )
35 11 28 lspid ⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) = ( ⊥ ‘ 𝑄 ) )
36 9 13 35 syl2anc ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) = ( ⊥ ‘ 𝑄 ) )
37 36 uneq1d ⊢ ( 𝜑 → ( ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
38 37 fveq2d ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
40 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → 𝑈 ∈ LMod )
41 8 11 lssss ⊢ ( ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) → ( ⊥ ‘ 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
42 13 41 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ⊥ ‘ 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
44 32 snssd ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) → { 𝑣 } ⊆ ( Base ‘ 𝑈 ) )
45 44 adantr ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → { 𝑣 } ⊆ ( Base ‘ 𝑈 ) )
46 45 adantl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → { 𝑣 } ⊆ ( Base ‘ 𝑈 ) )
47 8 28 lspun ⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ 𝑄 ) ⊆ ( Base ‘ 𝑈 ) ∧ { 𝑣 } ⊆ ( Base ‘ 𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
48 40 43 46 47 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ( LSpan ‘ 𝑈 ) ‘ ( ⊥ ‘ 𝑄 ) ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
49 uneq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) = ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
50 49 fveq2d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
51 50 adantl ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
53 39 48 52 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) )
54 eqid ⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
55 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
56 1 19 2 8 3 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
57 6 10 56 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
58 1 19 54 2 55 4 6 57 7 dihjat2 ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) = ( ( ⊥ ‘ 𝑄 ) ( LSSum ‘ 𝑈 ) 𝑄 ) )
59 1 2 8 54 6 42 10 djhcom ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) = ( 𝑄 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ 𝑄 ) ) )
60 11 4 9 7 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑈 ) )
61 11 28 55 lsmsp ⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑄 ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( ⊥ ‘ 𝑄 ) ( LSSum ‘ 𝑈 ) 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) )
62 9 13 60 61 syl3anc ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) ( LSSum ‘ 𝑈 ) 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) )
63 58 59 62 3eqtr3rd ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) = ( 𝑄 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ 𝑄 ) ) )
64 1 2 8 3 54 djhexmid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑄 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ 𝑄 ) ) = ( Base ‘ 𝑈 ) )
65 6 10 64 syl2anc ⊢ ( 𝜑 → ( 𝑄 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ 𝑄 ) ) = ( Base ‘ 𝑈 ) )
66 63 65 eqtrd ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) = ( Base ‘ 𝑈 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ 𝑄 ) ) = ( Base ‘ 𝑈 ) )
68 53 67 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) )
69 68 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) ) )
70 34 69 jcad ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) ) ) )
71 70 reximdv2 ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) ) )
72 31 71 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) )
73 1 2 6 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
74 8 28 11 5 islshp ⊢ ( 𝑈 ∈ LVec → ( ( ⊥ ‘ 𝑄 ) ∈ 𝑌 ↔ ( ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( ⊥ ‘ 𝑄 ) ≠ ( Base ‘ 𝑈 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) ) ) )
75 73 74 syl ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑄 ) ∈ 𝑌 ↔ ( ( ⊥ ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( ⊥ ‘ 𝑄 ) ≠ ( Base ‘ 𝑈 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ ( ( ⊥ ‘ 𝑄 ) ∪ { 𝑣 } ) ) = ( Base ‘ 𝑈 ) ) ) )
76 13 27 72 75 mpbir3and ⊢ ( 𝜑 → ( ⊥ ‘ 𝑄 ) ∈ 𝑌 )