Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lshpnelb Structured version   Unicode version

Theorem lshpnelb 34182
 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.)
Hypotheses
Ref Expression
lshpnelb.v
lshpnelb.n
lshpnelb.p
lshpnelb.h LSHyp
lshpnelb.w
lshpnelb.u
lshpnelb.x
Assertion
Ref Expression
lshpnelb

Proof of Theorem lshpnelb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 lshpnelb.u . . . . . 6
2 lshpnelb.v . . . . . . 7
3 lshpnelb.n . . . . . . 7
4 eqid 2467 . . . . . . 7
5 lshpnelb.p . . . . . . 7
6 lshpnelb.h . . . . . . 7 LSHyp
7 lshpnelb.w . . . . . . . 8
8 lveclmod 17623 . . . . . . . 8
97, 8syl 16 . . . . . . 7
102, 3, 4, 5, 6, 9islshpsm 34178 . . . . . 6
111, 10mpbid 210 . . . . 5
1211simp3d 1010 . . . 4
14 simp1l 1020 . . . . . 6
15 simp2 997 . . . . . 6
164lsssssubg 17475 . . . . . . . . . . . 12 SubGrp
179, 16syl 16 . . . . . . . . . . 11 SubGrp
184, 6, 9, 1lshplss 34179 . . . . . . . . . . 11
1917, 18sseldd 3510 . . . . . . . . . 10 SubGrp
20 lshpnelb.x . . . . . . . . . . . 12
212, 4, 3lspsncl 17494 . . . . . . . . . . . 12
229, 20, 21syl2anc 661 . . . . . . . . . . 11
2317, 22sseldd 3510 . . . . . . . . . 10 SubGrp
245lsmub1 16549 . . . . . . . . . 10 SubGrp SubGrp
2519, 23, 24syl2anc 661 . . . . . . . . 9
2625adantr 465 . . . . . . . 8
275lsmub2 16550 . . . . . . . . . . . 12 SubGrp SubGrp
2819, 23, 27syl2anc 661 . . . . . . . . . . 11
292, 3lspsnid 17510 . . . . . . . . . . . 12
309, 20, 29syl2anc 661 . . . . . . . . . . 11
3128, 30sseldd 3510 . . . . . . . . . 10
32 nelne1 2796 . . . . . . . . . 10
3331, 32sylan 471 . . . . . . . . 9
3433necomd 2738 . . . . . . . 8
35 df-pss 3497 . . . . . . . 8
3626, 34, 35sylanbrc 664 . . . . . . 7
37363ad2ant1 1017 . . . . . 6
384, 5lsmcl 17600 . . . . . . . . . . . 12
399, 18, 22, 38syl3anc 1228 . . . . . . . . . . 11
402, 4lssss 17454 . . . . . . . . . . 11
4139, 40syl 16 . . . . . . . . . 10
4241adantr 465 . . . . . . . . 9
43 simpr 461 . . . . . . . . 9
4442, 43sseqtr4d 3546 . . . . . . . 8
4544adantlr 714 . . . . . . 7
46453adant2 1015 . . . . . 6
477adantr 465 . . . . . . 7
4818adantr 465 . . . . . . 7
4939adantr 465 . . . . . . 7
50 simpr 461 . . . . . . 7
512, 4, 3, 5, 47, 48, 49, 50lsmcv 17658 . . . . . 6
5214, 15, 37, 46, 51syl211anc 1234 . . . . 5
53 simp3 998 . . . . 5
5452, 53eqtrd 2508 . . . 4
5554rexlimdv3a 2961 . . 3
5613, 55mpd 15 . 2