This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ellspsn5 ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ 𝑄 ) ∈ 𝑌 ) ∧ 𝑣 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∧ 𝑣 ≠ ( 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 ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ( ⊥ ‘ 𝑄 ) ∈ 𝑌 ) )