Metamath Proof Explorer


Theorem cdlemn11a

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

Ref Expression
Hypotheses cdlemn11a.b B=BaseK
cdlemn11a.l ˙=K
cdlemn11a.j ˙=joinK
cdlemn11a.a A=AtomsK
cdlemn11a.h H=LHypK
cdlemn11a.p P=ocKW
cdlemn11a.o O=hTIB
cdlemn11a.t T=LTrnKW
cdlemn11a.r R=trLKW
cdlemn11a.e E=TEndoKW
cdlemn11a.i I=DIsoBKW
cdlemn11a.J J=DIsoCKW
cdlemn11a.u U=DVecHKW
cdlemn11a.d +˙=+U
cdlemn11a.s ˙=LSSumU
cdlemn11a.f F=ιhT|hP=Q
cdlemn11a.g G=ιhT|hP=N
Assertion cdlemn11a KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXGITJN

Proof

Step Hyp Ref Expression
1 cdlemn11a.b B=BaseK
2 cdlemn11a.l ˙=K
3 cdlemn11a.j ˙=joinK
4 cdlemn11a.a A=AtomsK
5 cdlemn11a.h H=LHypK
6 cdlemn11a.p P=ocKW
7 cdlemn11a.o O=hTIB
8 cdlemn11a.t T=LTrnKW
9 cdlemn11a.r R=trLKW
10 cdlemn11a.e E=TEndoKW
11 cdlemn11a.i I=DIsoBKW
12 cdlemn11a.J J=DIsoCKW
13 cdlemn11a.u U=DVecHKW
14 cdlemn11a.d +˙=+U
15 cdlemn11a.s ˙=LSSumU
16 cdlemn11a.f F=ιhT|hP=Q
17 cdlemn11a.g G=ιhT|hP=N
18 simp1 KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXKHLWH
19 2 4 5 6 lhpocnel2 KHLWHPA¬P˙W
20 19 3ad2ant1 KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXPA¬P˙W
21 simp22 KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXNA¬N˙W
22 2 4 5 8 17 ltrniotacl KHLWHPA¬P˙WNA¬N˙WGT
23 18 20 21 22 syl3anc KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXGT
24 fvresi GTITG=G
25 23 24 syl KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXITG=G
26 25 eqcomd KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXG=ITG
27 5 8 10 tendoidcl KHLWHITE
28 27 3ad2ant1 KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXITE
29 riotaex ιhT|hP=NV
30 17 29 eqeltri GV
31 8 fvexi TV
32 resiexg TVITV
33 31 32 ax-mp ITV
34 2 4 5 6 8 10 12 17 30 33 dicopelval2 KHLWHNA¬N˙WGITJNG=ITGITE
35 18 21 34 syl2anc KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXGITJNG=ITGITE
36 26 28 35 mpbir2and KHLWHQA¬Q˙WNA¬N˙WXBX˙WJNJQ˙IXGITJN