Metamath Proof Explorer


Theorem cdlemj2

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate p . (Contributed by NM, 20-Jun-2013)

Ref Expression
Hypotheses cdlemj.b B=BaseK
cdlemj.h H=LHypK
cdlemj.t T=LTrnKW
cdlemj.r R=trLKW
cdlemj.e E=TEndoKW
Assertion cdlemj2 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhUh=Vh

Proof

Step Hyp Ref Expression
1 cdlemj.b B=BaseK
2 cdlemj.h H=LHypK
3 cdlemj.t T=LTrnKW
4 cdlemj.r R=trLKW
5 cdlemj.e E=TEndoKW
6 simpl1 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWKHLWHUEVEUF=VFFTFIBhT
7 simpl2 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWhIBgTgIB
8 simpl3l KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWRFRg
9 simpl3r KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWRgRh
10 simpr KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWpAtomsK¬pKW
11 eqid K=K
12 eqid AtomsK=AtomsK
13 1 2 3 4 5 11 12 cdlemj1 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWUhp=Vhp
14 6 7 8 9 10 13 syl113anc KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWUhp=Vhp
15 14 exp32 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWUhp=Vhp
16 15 ralrimiv KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWUhp=Vhp
17 simp11 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhKHLWH
18 simp121 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhUE
19 simp133 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhhT
20 2 3 5 tendocl KHLWHUEhTUhT
21 17 18 19 20 syl3anc KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhUhT
22 simp122 KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhVE
23 2 3 5 tendocl KHLWHVEhTVhT
24 17 22 19 23 syl3anc KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhVhT
25 11 12 2 3 ltrneq KHLWHUhTVhTpAtomsK¬pKWUhp=VhpUh=Vh
26 17 21 24 25 syl3anc KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhpAtomsK¬pKWUhp=VhpUh=Vh
27 16 26 mpbid KHLWHUEVEUF=VFFTFIBhThIBgTgIBRFRgRgRhUh=Vh