Theorem lsatcv0

Description: An atom covers the zero subspace. ( atcv0 analog.) (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	lsatcv0.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatcv0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatcv0.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lsatcv0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatcv0.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	lsatcv0	⊢ ( 𝜑 → { 0 } 𝐶 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		lsatcv0.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lsatcv0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3		lsatcv0.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
4		lsatcv0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lsatcv0.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
6		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
7	4 6	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9	8 2 7 5	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
10	1 8	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ 𝑄 )
11	7 9 10	syl2anc	⊢ ( 𝜑 → { 0 } ⊆ 𝑄 )
12	1 2 7 5	lsatn0	⊢ ( 𝜑 → 𝑄 ≠ { 0 } )
13	12	necomd	⊢ ( 𝜑 → { 0 } ≠ 𝑄 )
14		df-pss	⊢ ( { 0 } ⊊ 𝑄 ↔ ( { 0 } ⊆ 𝑄 ∧ { 0 } ≠ 𝑄 ) )
15	11 13 14	sylanbrc	⊢ ( 𝜑 → { 0 } ⊊ 𝑄 )
16		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
17		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
18	16 17 1 2	islsat	⊢ ( 𝑊 ∈ LMod → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
19	7 18	syl	⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
20	5 19	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
21	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑊 ∈ LVec )
22		eldifi	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
24	16 1 8 17 21 23	lspsncv0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
25	24	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
26		psseq2	⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( 𝑠 ⊊ 𝑄 ↔ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
27	26	anbi2d	⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ↔ ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
28	27	rexbidv	⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ↔ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
29	28	notbid	⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ↔ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
30	29	biimprcd	⊢ ( ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) )
31	25 30	syl6	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) ) )
32	31	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) )
33	20 32	mpd	⊢ ( 𝜑 → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) )
34	1 8	lsssn0	⊢ ( 𝑊 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
35	7 34	syl	⊢ ( 𝜑 → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
36	8 3 4 35 9	lcvbr	⊢ ( 𝜑 → ( { 0 } 𝐶 𝑄 ↔ ( { 0 } ⊊ 𝑄 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) ) )
37	15 33 36	mpbir2and	⊢ ( 𝜑 → { 0 } 𝐶 𝑄 )