Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemg13a Structured version   Unicode version

Theorem cdlemg13a 33927
Description: TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
Hypotheses
Ref Expression
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
Ref Expression
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 of Theorem cdlemg13a
StepHypRef Expression
1 simp11l 1116 . . . . 5  |-  ( ( ( ( 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 )
2 simp12l 1118 . . . . 5  |-  ( ( ( ( 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 )
3 simp11 1035 . . . . . 6  |-  ( ( ( ( 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 ) )
4 simp2r 1032 . . . . . 6  |-  ( ( ( ( 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 )
5 cdlemg12.l . . . . . . 7  |-  .<_  =  ( le `  K )
6 cdlemg12.a . . . . . . 7  |-  A  =  ( Atoms `  K )
7 cdlemg12.h . . . . . . 7  |-  H  =  ( LHyp `  K
)
8 cdlemg12.t . . . . . . 7  |-  T  =  ( ( LTrn `  K
) `  W )
95, 6, 7, 8ltrnat 33414 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  P  e.  A
)  ->  ( G `  P )  e.  A
)
103, 4, 2, 9syl3anc 1264 . . . . 5  |-  ( ( ( ( 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
)
11 cdlemg12.j . . . . . 6  |-  .\/  =  ( join `  K )
125, 11, 6hlatlej1 32649 . . . . 5  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( G `  P )  e.  A )  ->  P  .<_  ( P  .\/  ( G `  P ) ) )
131, 2, 10, 12syl3anc 1264 . . . 4  |-  ( ( ( ( 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 ) ) )
14 simp32 1042 . . . . . . 7  |-  ( ( ( ( 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 ) )
15 simp2l 1031 . . . . . . . 8  |-  ( ( ( ( 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 )
16 simp12 1036 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
175, 6, 7, 8ltrnel 33413 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( G `  P )  e.  A  /\  -.  ( G `  P )  .<_  W ) )
183, 4, 16, 17syl3anc 1264 . . . . . . . 8  |-  ( ( ( ( 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 ) )
19 cdlemg12.m . . . . . . . . 9  |-  ./\  =  ( meet `  K )
20 cdlemg12b.r . . . . . . . . 9  |-  R  =  ( ( trL `  K
) `  W )
215, 11, 19, 6, 7, 8, 20trlval2 33438 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( G `  P )  e.  A  /\  -.  ( G `  P )  .<_  W ) )  ->  ( R `  F )  =  ( ( ( G `  P )  .\/  ( F `  ( G `  P ) ) ) 
./\  W ) )
223, 15, 18, 21syl3anc 1264 . . . . . . 7  |-  ( ( ( ( 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 ) )
235, 11, 19, 6, 7, 8, 20trlval2 33438 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  G )  =  ( ( P  .\/  ( G `  P )
)  ./\  W )
)
243, 4, 16, 23syl3anc 1264 . . . . . . 7  |-  ( ( ( ( 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 )
)
2514, 22, 243eqtr3d 2478 . . . . . 6  |-  ( ( ( ( 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 ) )
2625oveq2d 6321 . . . . 5  |-  ( ( ( ( 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 ) ) )
275, 6, 7, 8ltrncoat 33418 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  P  e.  A )  ->  ( F `  ( G `  P ) )  e.  A )
283, 15, 4, 2, 27syl121anc 1269 . . . . . 6  |-  ( ( ( ( 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 2429 . . . . . . 7  |-  ( ( ( G `  P
)  .\/  ( F `  ( G `  P
) ) )  ./\  W )  =  ( ( ( G `  P
)  .\/  ( F `  ( G `  P
) ) )  ./\  W )
305, 11, 19, 6, 7, 29cdleme0cp 33489 . . . . . 6  |-  ( ( ( 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 ) ) ) )
313, 18, 28, 30syl12anc 1262 . . . . 5  |-  ( ( ( ( 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 2429 . . . . . . 7  |-  ( ( P  .\/  ( G `
 P ) ) 
./\  W )  =  ( ( P  .\/  ( G `  P ) )  ./\  W )
335, 11, 19, 6, 7, 32cdleme0cq 33490 . . . . . 6  |-  ( ( ( 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 ) ) )
343, 2, 18, 33syl12anc 1262 . . . . 5  |-  ( ( ( ( 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 ) ) )
3526, 31, 343eqtr3rd 2479 . . . 4  |-  ( ( ( ( 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
) ) ) )
3613, 35breqtrd 4450 . . 3  |-  ( ( ( ( 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
) ) ) )
375, 11, 6hlatlej2 32650 . . . 4  |-  ( ( K  e.  HL  /\  ( G `  P )  e.  A  /\  ( F `  ( G `  P ) )  e.  A )  ->  ( F `  ( G `  P ) )  .<_  ( ( G `  P )  .\/  ( F `  ( G `  P ) ) ) )
381, 10, 28, 37syl3anc 1264 . . 3  |-  ( ( ( ( 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 hllat 32638 . . . . 5  |-  ( K  e.  HL  ->  K  e.  Lat )
401, 39syl 17 . . . 4  |-  ( ( ( ( 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 )
41 eqid 2429 . . . . . 6  |-  ( Base `  K )  =  (
Base `  K )
4241, 6atbase 32564 . . . . 5  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
432, 42syl 17 . . . 4  |-  ( ( ( ( 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 )
)
4441, 6atbase 32564 . . . . 5  |-  ( ( F `  ( G `
 P ) )  e.  A  ->  ( F `  ( G `  P ) )  e.  ( Base `  K
) )
4528, 44syl 17 . . . 4  |-  ( ( ( ( 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 )
)
4641, 11, 6hlatjcl 32641 . . . . 5  |-  ( ( K  e.  HL  /\  ( G `  P )  e.  A  /\  ( F `  ( G `  P ) )  e.  A )  ->  (
( G `  P
)  .\/  ( F `  ( G `  P
) ) )  e.  ( Base `  K
) )
471, 10, 28, 46syl3anc 1264 . . . 4  |-  ( ( ( ( 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 )
)
4841, 5, 11latjle12 16259 . . . 4  |-  ( ( 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 )
) ) ) )
4940, 43, 45, 47, 48syl13anc 1266 . . 3  |-  ( ( ( ( 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 )
) ) ) )
5036, 38, 49mpbi2and 929 . 2  |-  ( ( ( ( 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 ) ) ) )
51 simp13 1037 . . . . 5  |-  ( ( ( ( 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 ) )
52 simp33 1043 . . . . 5  |-  ( ( ( ( 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 ) )
535, 11, 19, 6, 7, 8cdlemg11a 33913 . . . . 5  |-  ( ( ( 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 )
543, 16, 51, 15, 4, 52, 53syl123anc 1281 . . . 4  |-  ( ( ( ( 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
)
5554necomd 2702 . . 3  |-  ( ( ( ( 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 ) ) )
565, 11, 6ps-1 32751 . . 3  |-  ( ( 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
) ) ) ) )
571, 2, 28, 55, 10, 28, 56syl132anc 1282 . 2  |-  ( ( ( ( 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
) ) ) ) )
5850, 57mpbid 213 1  |-  ( ( ( ( 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
) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870    =/= wne 2625   class class class wbr 4426   ` cfv 5601  (class class class)co 6305   Basecbs 15084   lecple 15159   joincjn 16140   meetcmee 16141   Latclat 16242   Atomscatm 32538   HLchlt 32625   LHypclh 33258   LTrncltrn 33375   trLctrl 33433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-riotaBAD 32234
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-undef 7028  df-map 7482  df-preset 16124  df-poset 16142  df-plt 16155  df-lub 16171  df-glb 16172  df-join 16173  df-meet 16174  df-p0 16236  df-p1 16237  df-lat 16243  df-clat 16305  df-oposet 32451  df-ol 32453  df-oml 32454  df-covers 32541  df-ats 32542  df-atl 32573  df-cvlat 32597  df-hlat 32626  df-llines 32772  df-lplanes 32773  df-lvols 32774  df-lines 32775  df-psubsp 32777  df-pmap 32778  df-padd 33070  df-lhyp 33262  df-laut 33263  df-ldil 33378  df-ltrn 33379  df-trl 33434
This theorem is referenced by:  cdlemg13  33928
  Copyright terms: Public domain W3C validator