Theorem lcv1

Description: Covering property of a subspace plus an atom. ( chcv1 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lcv1.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lcv1.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lcv1.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lcv1.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lcv1.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lcv1.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lcv1.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	lcv1	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcv1.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lcv1.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
3		lcv1.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lcv1.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5		lcv1.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lcv1.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		lcv1.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
10		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
11	8 9 10 3	islsat	⊢ ( 𝑊 ∈ LVec → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
12	5 11	syl	⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
13	7 12	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
15	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑊 ∈ LVec )
16	15	3ad2ant1	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → 𝑊 ∈ LVec )
17	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑈 ∈ 𝑆 )
18	17	3ad2ant1	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → 𝑈 ∈ 𝑆 )
19		eldifi	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
20	19	3ad2ant2	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
21		simp1r	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → ¬ 𝑄 ⊆ 𝑈 )
22		simp3	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
23	22	sseq1d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → ( 𝑄 ⊆ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) )
24	21 23	mtbid	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → ¬ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 )
25	8 1 9 2 4 16 18 20 24	lsmcv2	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → 𝑈 𝐶 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
26	22	oveq2d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → ( 𝑈 ⊕ 𝑄 ) = ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
27	25 26	breqtrrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) )
28	27	rexlimdv3a	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → ( ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )
29	14 28	mpd	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) )
30	5	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → 𝑊 ∈ LVec )
31	6	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → 𝑈 ∈ 𝑆 )
32		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
33	5 32	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
34	1 3 33 7	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
35	1 2	lsmcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆 ) → ( 𝑈 ⊕ 𝑄 ) ∈ 𝑆 )
36	33 6 34 35	syl3anc	⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑄 ) ∈ 𝑆 )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → ( 𝑈 ⊕ 𝑄 ) ∈ 𝑆 )
38		simpr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) )
39	1 4 30 31 37 38	lcvpss	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) )
40	1	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
41	33 40	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
42	41 6	sseldd	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
43	41 34	sseldd	⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
44	2 42 43	lssnle	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) ) )
46	39 45	mpbird	⊢ ( ( 𝜑 ∧ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) → ¬ 𝑄 ⊆ 𝑈 )
47	29 46	impbida	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )