This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemg13a

Description: TODO: FIX COMMENT. (Contributed by NM, 6-May-2013)

Ref Expression
Hypotheses cdlemg12.l 
|- .<_ = ( le ` K )
cdlemg12.j 
|- .\/ = ( join ` K )
cdlemg12.m 
|- ./\ = ( meet ` K )
cdlemg12.a 
|- A = ( Atoms ` K )
cdlemg12.h 
|- H = ( LHyp ` K )
cdlemg12.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemg12b.r 
|- R = ( ( trL ` K ) ` W )
Assertion cdlemg13a 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemg12.l 
 |-  .<_ = ( le ` K )
2 cdlemg12.j 
 |-  .\/ = ( join ` K )
3 cdlemg12.m 
 |-  ./\ = ( meet ` K )
4 cdlemg12.a 
 |-  A = ( Atoms ` K )
5 cdlemg12.h 
 |-  H = ( LHyp ` K )
6 cdlemg12.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemg12b.r 
 |-  R = ( ( trL ` K ) ` W )
8 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> K e. HL )
9 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> P e. A )
10 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
11 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> G e. T )
12 1 4 5 6 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
13 10 11 9 12 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( G ` P ) e. A )
14 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ ( G ` P ) e. A ) -> P .<_ ( P .\/ ( G ` P ) ) )
15 8 9 13 14 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> P .<_ ( P .\/ ( G ` P ) ) )
16 simp32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( R ` F ) = ( R ` G ) )
17 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> F e. T )
18 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( P e. A /\ -. P .<_ W ) )
19 1 4 5 6 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
20 10 11 18 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
21 1 2 3 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) -> ( R ` F ) = ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
22 10 17 20 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( R ` F ) = ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
23 1 2 3 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
24 10 11 18 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
25 16 22 24 3eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
26 25 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( G ` P ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) = ( ( G ` P ) .\/ ( ( P .\/ ( G ` P ) ) ./\ W ) ) )
27 1 4 5 6 ltrncoat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ P e. A ) -> ( F ` ( G ` P ) ) e. A )
28 10 17 11 9 27 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( F ` ( G ` P ) ) e. A )
29 eqid 
 |-  ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W )
30 1 2 3 4 5 29 cdleme0cp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) /\ ( F ` ( G ` P ) ) e. A ) ) -> ( ( G ` P ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
31 10 20 28 30 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( G ` P ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
32 eqid 
 |-  ( ( P .\/ ( G ` P ) ) ./\ W ) = ( ( P .\/ ( G ` P ) ) ./\ W )
33 1 2 3 4 5 32 cdleme0cq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) ) -> ( ( G ` P ) .\/ ( ( P .\/ ( G ` P ) ) ./\ W ) ) = ( P .\/ ( G ` P ) ) )
34 10 9 20 33 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( G ` P ) .\/ ( ( P .\/ ( G ` P ) ) ./\ W ) ) = ( P .\/ ( G ` P ) ) )
35 26 31 34 3eqtr3rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( P .\/ ( G ` P ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
36 15 35 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> P .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
37 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ ( G ` P ) e. A /\ ( F ` ( G ` P ) ) e. A ) -> ( F ` ( G ` P ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
38 8 13 28 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( F ` ( G ` P ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
39 8 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> K e. Lat )
40 eqid 
 |-  ( Base ` K ) = ( Base ` K )
41 40 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
42 9 41 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> P e. ( Base ` K ) )
43 40 4 atbase 
 |-  ( ( F ` ( G ` P ) ) e. A -> ( F ` ( G ` P ) ) e. ( Base ` K ) )
44 28 43 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( F ` ( G ` P ) ) e. ( Base ` K ) )
45 40 2 4 hlatjcl 
 |-  ( ( K e. HL /\ ( G ` P ) e. A /\ ( F ` ( G ` P ) ) e. A ) -> ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
46 8 13 28 45 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
47 40 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ ( F ` ( G ` P ) ) e. ( Base ` K ) /\ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) /\ ( F ` ( G ` P ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) <-> ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) )
48 39 42 44 46 47 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( P .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) /\ ( F ` ( G ` P ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) <-> ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) )
49 36 38 48 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )
50 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
51 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) )
52 1 2 3 4 5 6 cdlemg11a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( F ` ( G ` P ) ) =/= P )
53 10 18 50 17 11 51 52 syl123anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( F ` ( G ` P ) ) =/= P )
54 53 necomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> P =/= ( F ` ( G ` P ) ) )
55 1 2 4 ps-1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( F ` ( G ` P ) ) e. A /\ P =/= ( F ` ( G ` P ) ) ) /\ ( ( G ` P ) e. A /\ ( F ` ( G ` P ) ) e. A ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) <-> ( P .\/ ( F ` ( G ` P ) ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) )
56 8 9 28 54 13 28 55 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) <-> ( P .\/ ( F ` ( G ` P ) ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) )
57 49 56 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) = ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) )