Theorem lsmcv2

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of Kalmbach p. 153. ( spansncv2 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsmcv2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsmcv2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lsmcv2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsmcv2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lsmcv2.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lsmcv2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsmcv2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lsmcv2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lsmcv2.l	⊢ ( 𝜑 → ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
Assertion	lsmcv2	⊢ ( 𝜑 → 𝑈 𝐶 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsmcv2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsmcv2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lsmcv2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lsmcv2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
5		lsmcv2.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
6		lsmcv2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
7		lsmcv2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8		lsmcv2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		lsmcv2.l	⊢ ( 𝜑 → ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
10		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	6 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12	2	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
13	11 12	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
14	13 7	sseldd	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
15	1 2 3	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
16	11 8 15	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
17	13 16	sseldd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
18	4 14 17	lssnle	⊢ ( 𝜑 → ( ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ↔ 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) )
19	9 18	mpbid	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
20		3simpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) )
21		simp3l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) → 𝑈 ⊊ 𝑥 )
22		simp3r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) → 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
23	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ LVec )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑈 ∈ 𝑆 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
26	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 ∈ 𝑉 )
27	1 2 3 4 23 24 25 26	lsmcv	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑥 = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
28	20 21 22 27	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) → 𝑥 = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
29	28	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → ( ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑥 = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) )
30	29	ralrimiv	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑥 = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) )
31	2 4	lsmcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝑆 )
32	11 7 16 31	syl3anc	⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝑆 )
33	2 5 6 7 32	lcvbr2	⊢ ( 𝜑 → ( 𝑈 𝐶 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ( 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝑈 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑥 = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) ) )
34	19 30 33	mpbir2and	⊢ ( 𝜑 → 𝑈 𝐶 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )