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 = LHyp K
cdlemg44.t T = LTrn K W
cdlemg44.r R = trL K W
Assertion cdlemg44 K HL W H F T G T R F R G F G = G F

Proof

Step Hyp Ref Expression
1 cdlemg44.h H = LHyp K
2 cdlemg44.t T = LTrn K W
3 cdlemg44.r R = trL K W
4 eqid K = K
5 eqid Atoms K = Atoms K
6 4 5 1 lhpexnle K HL W H p Atoms K ¬ p K W
7 6 3ad2ant1 K HL W H F T G T R F R G p Atoms K ¬ p K W
8 simp11 K HL W H F T G T R F R G p Atoms K ¬ p K W K HL W H
9 simp12l K HL W H F T G T R F R G p Atoms K ¬ p K W F T
10 simp12r K HL W H F T G T R F R G p Atoms K ¬ p K W G T
11 1 2 ltrnco K HL W H F T G T F G T
12 8 9 10 11 syl3anc K HL W H F T G T R F R G p Atoms K ¬ p K W F G T
13 1 2 ltrnco K HL W H G T F T G F T
14 8 10 9 13 syl3anc K HL W H F T G T R F R G p Atoms K ¬ p K W G F T
15 3simpc K HL W H F T G T R F R G p Atoms K ¬ p K W p Atoms K ¬ p K W
16 simp13 K HL W H F T G T R F R G p Atoms K ¬ p K W R F R G
17 1 2 3 4 5 cdlemg44b K HL W H F T G T p Atoms K ¬ p K W R F R G F G p = G F p
18 8 9 10 15 16 17 syl131anc K HL W H F T G T R F R G p Atoms K ¬ p K W F G p = G F p
19 simp12 K HL W H F T G T R F R G p Atoms K ¬ p K W F T G T
20 simp2 K HL W H F T G T R F R G p Atoms K ¬ p K W p Atoms K
21 4 5 1 2 ltrncoval K HL W H F T G T p Atoms K F G p = F G p
22 8 19 20 21 syl3anc K HL W H F T G T R F R G p Atoms K ¬ p K W F G p = F G p
23 4 5 1 2 ltrncoval K HL W H G T F T p Atoms K G F p = G F p
24 8 10 9 20 23 syl121anc K HL W H F T G T R F R G p Atoms K ¬ p K W G F p = G F p
25 18 22 24 3eqtr4d K HL W H F T G T R F R G p Atoms K ¬ p K W F G p = G F p
26 4 5 1 2 cdlemd K HL W H F G T G F T p Atoms K ¬ p K W F G p = G F p F G = G F
27 8 12 14 15 25 26 syl311anc K HL W H F T G T R F R G p Atoms K ¬ p K W F G = G F
28 27 rexlimdv3a K HL W H F T G T R F R G p Atoms K ¬ p K W F G = G F
29 7 28 mpd K HL W H F T G T R F R G F G = G F