Theorem lsatcveq0

Description: A subspace covered by an atom must be the zero subspace. ( atcveq0 analog.) (Contributed by NM, 7-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatcveq0.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lsatcveq0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lsatcveq0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lsatcveq0.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5		lsatcveq0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lsatcveq0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		lsatcveq0.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8	5	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑊 ∈ LVec )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑈 ∈ 𝑆 )
10		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	5 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12	2 3 11 7	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑄 ∈ 𝑆 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑈 𝐶 𝑄 )
15	2 4 8 9 13 14	lcvpss	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑈 ⊊ 𝑄 )
16	15	ex	⊢ ( 𝜑 → ( 𝑈 𝐶 𝑄 → 𝑈 ⊊ 𝑄 ) )
17	1 3 4 5 7	lsatcv0	⊢ ( 𝜑 → { 0 } 𝐶 𝑄 )
18	5	3ad2ant1	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑊 ∈ LVec )
19	1 2	lsssn0	⊢ ( 𝑊 ∈ LMod → { 0 } ∈ 𝑆 )
20	11 19	syl	⊢ ( 𝜑 → { 0 } ∈ 𝑆 )
21	20	3ad2ant1	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → { 0 } ∈ 𝑆 )
22	12	3ad2ant1	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑄 ∈ 𝑆 )
23	6	3ad2ant1	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑈 ∈ 𝑆 )
24		simp2	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → { 0 } 𝐶 𝑄 )
25	1 2	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → { 0 } ⊆ 𝑈 )
26	11 6 25	syl2anc	⊢ ( 𝜑 → { 0 } ⊆ 𝑈 )
27	26	3ad2ant1	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → { 0 } ⊆ 𝑈 )
28		simp3	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑈 ⊊ 𝑄 )
29	2 4 18 21 22 23 24 27 28	lcvnbtwn3	⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑈 = { 0 } )
30	29	3exp	⊢ ( 𝜑 → ( { 0 } 𝐶 𝑄 → ( 𝑈 ⊊ 𝑄 → 𝑈 = { 0 } ) ) )
31	17 30	mpd	⊢ ( 𝜑 → ( 𝑈 ⊊ 𝑄 → 𝑈 = { 0 } ) )
32	16 31	syld	⊢ ( 𝜑 → ( 𝑈 𝐶 𝑄 → 𝑈 = { 0 } ) )
33		breq1	⊢ ( 𝑈 = { 0 } → ( 𝑈 𝐶 𝑄 ↔ { 0 } 𝐶 𝑄 ) )
34	17 33	syl5ibrcom	⊢ ( 𝜑 → ( 𝑈 = { 0 } → 𝑈 𝐶 𝑄 ) )
35	32 34	impbid	⊢ ( 𝜑 → ( 𝑈 𝐶 𝑄 ↔ 𝑈 = { 0 } ) )