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

Metamath Proof Explorer

Theorem lsat0cv

Description: A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses lsat0cv.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsat0cv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsat0cv.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsat0cv.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lsat0cv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsat0cv.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion lsat0cv ( 𝜑 → ( 𝑈 ∈ 𝐴 ↔ { 0 } 𝐶 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsat0cv.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsat0cv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsat0cv.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lsat0cv.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5 lsat0cv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lsat0cv.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 5 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐴 ) → 𝑊 ∈ LVec )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ∈ 𝐴 )
9 1 3 4 7 8 lsatcv0 ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐴 ) → { 0 } 𝐶 𝑈 )
10 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 5 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 11 adantr ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → 𝑊 ∈ LMod )
13 1 2 lsssn0 ⊢ ( 𝑊 ∈ LMod → { 0 } ∈ 𝑆 )
14 11 13 syl ⊢ ( 𝜑 → { 0 } ∈ 𝑆 )
15 14 adantr ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → { 0 } ∈ 𝑆 )
16 6 adantr ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → 𝑈 ∈ 𝑆 )
17 simpr ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → { 0 } 𝐶 𝑈 )
18 2 4 12 15 16 17 lcvpss ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → { 0 } ⊊ 𝑈 )
19 pssnel ⊢ ( { 0 } ⊊ 𝑈 → ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) )
20 18 19 syl ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) )
21 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) ) → 𝑈 ∈ 𝑆 )
22 simprl ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) ) → 𝑥 ∈ 𝑈 )
23 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
24 23 2 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
25 21 22 24 syl2anc ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
26 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
27 26 biimpri ⊢ ( 𝑥 = 0 → 𝑥 ∈ { 0 } )
28 27 necon3bi ⊢ ( ¬ 𝑥 ∈ { 0 } → 𝑥 ≠ 0 )
29 28 adantl ⊢ ( ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) → 𝑥 ≠ 0 )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) ) → 𝑥 ≠ 0 )
31 eldifsn ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ≠ 0 ) )
32 25 30 31 sylanbrc ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) ) → 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) )
33 32 22 jca ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) ) → ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑥 ∈ 𝑈 ) )
34 33 ex ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ( ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) → ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑥 ∈ 𝑈 ) ) )
35 34 eximdv ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) → ∃ 𝑥 ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑥 ∈ 𝑈 ) ) )
36 df-rex ⊢ ( ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑥 ∈ 𝑈 ↔ ∃ 𝑥 ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑥 ∈ 𝑈 ) )
37 35 36 imbitrrdi ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 } ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑥 ∈ 𝑈 ) )
38 20 37 mpd ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑥 ∈ 𝑈 )
39 simpllr ⊢ ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) → { 0 } 𝐶 𝑈 )
40 2 4 5 14 6 lcvbr2 ⊢ ( 𝜑 → ( { 0 } 𝐶 𝑈 ↔ ( { 0 } ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ( { 0 } 𝐶 𝑈 ↔ ( { 0 } ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) ) ) )
42 41 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) → ( { 0 } 𝐶 𝑈 ↔ ( { 0 } ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) ) ) )
43 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑊 ∈ LMod )
44 43 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → 𝑊 ∈ LMod )
45 eldifi ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
46 45 adantl ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
47 46 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
48 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
49 23 2 48 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝑆 )
50 44 47 49 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝑆 )
51 1 2 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝑆 ) → { 0 } ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
52 44 50 51 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → { 0 } ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
53 eldifsni ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → 𝑥 ≠ 0 )
54 53 adantl ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑥 ≠ 0 )
55 54 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → 𝑥 ≠ 0 )
56 23 1 48 lspsneq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = { 0 } ↔ 𝑥 = 0 ) )
57 44 47 56 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = { 0 } ↔ 𝑥 = 0 ) )
58 57 necon3bid ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ≠ { 0 } ↔ 𝑥 ≠ 0 ) )
59 55 58 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ≠ { 0 } )
60 59 necomd ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → { 0 } ≠ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
61 df-pss ⊢ ( { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ↔ ( { 0 } ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∧ { 0 } ≠ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
62 52 60 61 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
63 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑈 ∈ 𝑆 )
64 63 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → 𝑈 ∈ 𝑆 )
65 simplr ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → 𝑥 ∈ 𝑈 )
66 2 48 44 64 65 ellspsn5 ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 )
67 62 66 jca ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) )
68 psseq2 ⊢ ( 𝑠 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( { 0 } ⊊ 𝑠 ↔ { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
69 sseq1 ⊢ ( 𝑠 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( 𝑠 ⊆ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) )
70 68 69 anbi12d ⊢ ( 𝑠 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ↔ ( { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) ) )
71 eqeq1 ⊢ ( 𝑠 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( 𝑠 = 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) )
72 70 71 imbi12d ⊢ ( 𝑠 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) ↔ ( ( { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) ) )
73 72 rspcv ⊢ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝑆 → ( ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) → ( ( { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) ) )
74 50 73 syl ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) → ( ( { 0 } ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) ) )
75 67 74 mpid ⊢ ( ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) ∧ { 0 } ⊊ 𝑈 ) → ( ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) )
76 75 expimpd ⊢ ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( { 0 } ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) )
77 42 76 sylbid ⊢ ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) → ( { 0 } 𝐶 𝑈 → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 ) )
78 39 77 mpd ⊢ ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) = 𝑈 )
79 78 eqcomd ⊢ ( ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
80 79 ex ⊢ ( ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ( 𝑥 ∈ 𝑈 → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
81 80 reximdva ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ( ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑥 ∈ 𝑈 → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
82 38 81 mpd ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
83 5 adantr ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → 𝑊 ∈ LVec )
84 23 48 1 3 islsat ⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
85 83 84 syl ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
86 82 85 mpbird ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑈 ) → 𝑈 ∈ 𝐴 )
87 9 86 impbida ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ↔ { 0 } 𝐶 𝑈 ) )