Metamath Proof Explorer


Theorem cdlemn

Description: Lemma N of Crawley p. 121 line 27. (Contributed by NM, 27-Feb-2014)

Ref Expression
Hypotheses cdlemn11.b B=BaseK
cdlemn11.l ˙=K
cdlemn11.j ˙=joinK
cdlemn11.a A=AtomsK
cdlemn11.h H=LHypK
cdlemn11.i I=DIsoBKW
cdlemn11.J J=DIsoCKW
cdlemn11.u U=DVecHKW
cdlemn11.s ˙=LSSumU
Assertion cdlemn KHLWHQA¬Q˙WRA¬R˙WXBX˙WR˙Q˙XJRJQ˙IX

Proof

Step Hyp Ref Expression
1 cdlemn11.b B=BaseK
2 cdlemn11.l ˙=K
3 cdlemn11.j ˙=joinK
4 cdlemn11.a A=AtomsK
5 cdlemn11.h H=LHypK
6 cdlemn11.i I=DIsoBKW
7 cdlemn11.J J=DIsoCKW
8 cdlemn11.u U=DVecHKW
9 cdlemn11.s ˙=LSSumU
10 1 2 3 4 5 8 9 6 7 cdlemn5 KHLWHQA¬Q˙WRA¬R˙WXBX˙WR˙Q˙XJRJQ˙IX
11 10 3expia KHLWHQA¬Q˙WRA¬R˙WXBX˙WR˙Q˙XJRJQ˙IX
12 1 2 3 4 5 6 7 8 9 cdlemn11 KHLWHQA¬Q˙WRA¬R˙WXBX˙WJRJQ˙IXR˙Q˙X
13 12 3expia KHLWHQA¬Q˙WRA¬R˙WXBX˙WJRJQ˙IXR˙Q˙X
14 11 13 impbid KHLWHQA¬Q˙WRA¬R˙WXBX˙WR˙Q˙XJRJQ˙IX