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

Theorem lsatcv0eq 29907
 Description: If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 23884 analog.) (Contributed by NM, 10-Jan-2015.)
Hypotheses
Ref Expression
lsatcv0eq.o
lsatcv0eq.p
lsatcv0eq.a LSAtoms
lsatcv0eq.c L
lsatcv0eq.w
lsatcv0eq.q
lsatcv0eq.r
Assertion
Ref Expression
lsatcv0eq

Proof of Theorem lsatcv0eq
StepHypRef Expression
1 lsatcv0eq.o . . . . . 6
2 lsatcv0eq.a . . . . . 6 LSAtoms
3 lsatcv0eq.w . . . . . 6
4 lsatcv0eq.q . . . . . 6
5 lsatcv0eq.r . . . . . 6
61, 2, 3, 4, 5lsatnem0 29905 . . . . 5
7 eqid 2438 . . . . . 6
8 lsatcv0eq.p . . . . . 6
9 lsatcv0eq.c . . . . . 6 L
10 lveclmod 16180 . . . . . . . 8
113, 10syl 16 . . . . . . 7
127, 2, 11, 4lsatlssel 29857 . . . . . 6
137, 8, 1, 2, 9, 3, 12, 5lcvp 29900 . . . . 5
141, 2, 9, 3, 4lsatcv0 29891 . . . . . 6
1514biantrurd 496 . . . . 5
166, 13, 153bitrd 272 . . . 4
173adantr 453 . . . . . 6
181, 7lsssn0 16026 . . . . . . . 8
1911, 18syl 16 . . . . . . 7
2019adantr 453 . . . . . 6
2112adantr 453 . . . . . 6
227, 2, 11, 5lsatlssel 29857 . . . . . . . 8
237, 8lsmcl 16157 . . . . . . . 8
2411, 12, 22, 23syl3anc 1185 . . . . . . 7
2524adantr 453 . . . . . 6
26 simprl 734 . . . . . 6
27 simprr 735 . . . . . 6
287, 9, 17, 20, 21, 25, 26, 27lcvntr 29886 . . . . 5
2928ex 425 . . . 4
3016, 29sylbid 208 . . 3