Metamath Proof Explorer

Theorem lshpnelb

Description: The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014)

Ref Expression
Hypotheses lshpnelb.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpnelb.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpnelb.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpnelb.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpnelb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpnelb.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
lshpnelb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion lshpnelb ( 𝜑 → ( ¬ 𝑋 ∈ 𝑈 ↔ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )

Proof

Step Hyp Ref Expression
1 lshpnelb.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpnelb.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lshpnelb.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lshpnelb.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5 lshpnelb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lshpnelb.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
7 lshpnelb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 5 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 1 2 8 3 4 10 islshpsm ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )
12 6 11 mpbid ⊢ ( 𝜑 → ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) )
13 12 simp3d ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 )
15 simp1l ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → 𝜑 )
16 simp2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑣 ∈ 𝑉 )
17 8 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
18 10 17 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
19 8 4 10 6 lshplss ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
20 18 19 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
21 1 8 2 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
22 10 7 21 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
23 18 22 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
24 3 lsmub1 ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑈 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
25 20 23 24 syl2anc ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑈 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
27 3 lsmub2 ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
28 20 23 27 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
29 1 2 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
30 10 7 29 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
31 28 30 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
32 nelne1 ⊢ ( ( 𝑋 ∈ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∧ ¬ 𝑋 ∈ 𝑈 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ≠ 𝑈 )
33 31 32 sylan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ≠ 𝑈 )
34 33 necomd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑈 ≠ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
35 df-pss ⊢ ( 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ( 𝑈 ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑈 ≠ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) )
36 26 34 35 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
37 36 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
38 8 3 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
39 10 19 22 38 syl3anc ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
40 1 8 lssss ⊢ ( ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑉 )
41 39 40 syl ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑉 )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑉 )
43 simpr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 )
44 42 43 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) )
46 45 3adant2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) )
47 5 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ LVec )
48 19 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
49 39 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
50 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
51 1 8 2 3 47 48 49 50 lsmcv ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑈 ⊊ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) )
52 15 16 37 46 51 syl211anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) )
53 simp3 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 )
54 52 53 eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
55 54 rexlimdv3a ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )
56 14 55 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
57 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑊 ∈ LMod )
58 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑈 ∈ 𝐻 )
59 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑋 ∈ 𝑉 )
60 simpr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
61 1 2 3 4 57 58 59 60 lshpnel ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → ¬ 𝑋 ∈ 𝑈 )
62 56 61 impbida ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ 𝑈 ↔ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )