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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )