Metamath Proof Explorer


Theorem cdlemg44

Description: Part of proof of Lemma G of Crawley p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013)

Ref Expression
Hypotheses cdlemg44.h H=LHypK
cdlemg44.t T=LTrnKW
cdlemg44.r R=trLKW
Assertion cdlemg44 KHLWHFTGTRFRGFG=GF

Proof

Step Hyp Ref Expression
1 cdlemg44.h H=LHypK
2 cdlemg44.t T=LTrnKW
3 cdlemg44.r R=trLKW
4 eqid K=K
5 eqid AtomsK=AtomsK
6 4 5 1 lhpexnle KHLWHpAtomsK¬pKW
7 6 3ad2ant1 KHLWHFTGTRFRGpAtomsK¬pKW
8 simp11 KHLWHFTGTRFRGpAtomsK¬pKWKHLWH
9 simp12l KHLWHFTGTRFRGpAtomsK¬pKWFT
10 simp12r KHLWHFTGTRFRGpAtomsK¬pKWGT
11 1 2 ltrnco KHLWHFTGTFGT
12 8 9 10 11 syl3anc KHLWHFTGTRFRGpAtomsK¬pKWFGT
13 1 2 ltrnco KHLWHGTFTGFT
14 8 10 9 13 syl3anc KHLWHFTGTRFRGpAtomsK¬pKWGFT
15 3simpc KHLWHFTGTRFRGpAtomsK¬pKWpAtomsK¬pKW
16 simp13 KHLWHFTGTRFRGpAtomsK¬pKWRFRG
17 1 2 3 4 5 cdlemg44b KHLWHFTGTpAtomsK¬pKWRFRGFGp=GFp
18 8 9 10 15 16 17 syl131anc KHLWHFTGTRFRGpAtomsK¬pKWFGp=GFp
19 simp12 KHLWHFTGTRFRGpAtomsK¬pKWFTGT
20 simp2 KHLWHFTGTRFRGpAtomsK¬pKWpAtomsK
21 4 5 1 2 ltrncoval KHLWHFTGTpAtomsKFGp=FGp
22 8 19 20 21 syl3anc KHLWHFTGTRFRGpAtomsK¬pKWFGp=FGp
23 4 5 1 2 ltrncoval KHLWHGTFTpAtomsKGFp=GFp
24 8 10 9 20 23 syl121anc KHLWHFTGTRFRGpAtomsK¬pKWGFp=GFp
25 18 22 24 3eqtr4d KHLWHFTGTRFRGpAtomsK¬pKWFGp=GFp
26 4 5 1 2 cdlemd KHLWHFGTGFTpAtomsK¬pKWFGp=GFpFG=GF
27 8 12 14 15 25 26 syl311anc KHLWHFTGTRFRGpAtomsK¬pKWFG=GF
28 27 rexlimdv3a KHLWHFTGTRFRGpAtomsK¬pKWFG=GF
29 7 28 mpd KHLWHFTGTRFRGFG=GF