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

Theorem ps-1 35617
Description: The join of two atoms  R  .\/  S (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda] p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67. (Contributed by NM, 15-Nov-2011.)
Hypotheses
Ref Expression
ps1.l  |-  .<_  =  ( le `  K )
ps1.j  |-  .\/  =  ( join `  K )
ps1.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
ps-1  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  <->  ( P  .\/  Q )  =  ( R  .\/  S ) ) )

Proof of Theorem ps-1
StepHypRef Expression
1 oveq1 6277 . . . . . 6  |-  ( R  =  P  ->  ( R  .\/  S )  =  ( P  .\/  S
) )
21breq2d 4451 . . . . 5  |-  ( R  =  P  ->  (
( P  .\/  Q
)  .<_  ( R  .\/  S )  <->  ( P  .\/  Q )  .<_  ( P  .\/  S ) ) )
31eqeq2d 2468 . . . . 5  |-  ( R  =  P  ->  (
( P  .\/  Q
)  =  ( R 
.\/  S )  <->  ( P  .\/  Q )  =  ( P  .\/  S ) ) )
42, 3imbi12d 318 . . . 4  |-  ( R  =  P  ->  (
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( P  .\/  Q )  =  ( R  .\/  S
) )  <->  ( ( P  .\/  Q )  .<_  ( P  .\/  S )  ->  ( P  .\/  Q )  =  ( P 
.\/  S ) ) ) )
54eqcoms 2466 . . 3  |-  ( P  =  R  ->  (
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( P  .\/  Q )  =  ( R  .\/  S
) )  <->  ( ( P  .\/  Q )  .<_  ( P  .\/  S )  ->  ( P  .\/  Q )  =  ( P 
.\/  S ) ) ) )
6 simp3 996 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( P  .\/  Q )  .<_  ( R 
.\/  S ) )
7 simp1 994 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  K  e.  HL )
8 simp21 1027 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  P  e.  A )
9 simp3l 1022 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  R  e.  A )
10 ps1.j . . . . . . . . . . . . 13  |-  .\/  =  ( join `  K )
11 ps1.a . . . . . . . . . . . . 13  |-  A  =  ( Atoms `  K )
1210, 11hlatjcom 35508 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  P  e.  A  /\  R  e.  A )  ->  ( P  .\/  R
)  =  ( R 
.\/  P ) )
137, 8, 9, 12syl3anc 1226 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( P  .\/  R
)  =  ( R 
.\/  P ) )
14133ad2ant1 1015 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( P  .\/  R )  =  ( R  .\/  P ) )
15 hllat 35504 . . . . . . . . . . . . . . . 16  |-  ( K  e.  HL  ->  K  e.  Lat )
16153ad2ant1 1015 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  K  e.  Lat )
17 eqid 2454 . . . . . . . . . . . . . . . . 17  |-  ( Base `  K )  =  (
Base `  K )
1817, 11atbase 35430 . . . . . . . . . . . . . . . 16  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
198, 18syl 16 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  P  e.  ( Base `  K ) )
20 simp22 1028 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  Q  e.  A )
2117, 11atbase 35430 . . . . . . . . . . . . . . . 16  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
2220, 21syl 16 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  Q  e.  ( Base `  K ) )
23 simp3r 1023 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  S  e.  A )
2417, 10, 11hlatjcl 35507 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  R  e.  A  /\  S  e.  A )  ->  ( R  .\/  S
)  e.  ( Base `  K ) )
257, 9, 23, 24syl3anc 1226 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( R  .\/  S
)  e.  ( Base `  K ) )
26 ps1.l . . . . . . . . . . . . . . . 16  |-  .<_  =  ( le `  K )
2717, 26, 10latjle12 15894 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  Q  e.  ( Base `  K )  /\  ( R  .\/  S )  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  ( R  .\/  S )  /\  Q  .<_  ( R 
.\/  S ) )  <-> 
( P  .\/  Q
)  .<_  ( R  .\/  S ) ) )
2816, 19, 22, 25, 27syl13anc 1228 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .<_  ( R  .\/  S )  /\  Q  .<_  ( R 
.\/  S ) )  <-> 
( P  .\/  Q
)  .<_  ( R  .\/  S ) ) )
29 simpl 455 . . . . . . . . . . . . . 14  |-  ( ( P  .<_  ( R  .\/  S )  /\  Q  .<_  ( R  .\/  S
) )  ->  P  .<_  ( R  .\/  S
) )
3028, 29syl6bir 229 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  P  .<_  ( R  .\/  S
) ) )
3130adantr 463 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  P  .<_  ( R  .\/  S
) ) )
32 simpl1 997 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  ->  K  e.  HL )
33 simpl21 1072 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  ->  P  e.  A )
34 simpl3r 1050 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  ->  S  e.  A )
35 simpl3l 1049 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  ->  R  e.  A )
36 simpr 459 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  ->  P  =/=  R )
3726, 10, 11hlatexchb1 35533 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  S  e.  A  /\  R  e.  A
)  /\  P  =/=  R )  ->  ( P  .<_  ( R  .\/  S
)  <->  ( R  .\/  P )  =  ( R 
.\/  S ) ) )
3832, 33, 34, 35, 36, 37syl131anc 1239 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( P  .<_  ( R 
.\/  S )  <->  ( R  .\/  P )  =  ( R  .\/  S ) ) )
3931, 38sylibd 214 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( R  .\/  P )  =  ( R  .\/  S
) ) )
40393impia 1191 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( R  .\/  P )  =  ( R  .\/  S ) )
4114, 40eqtrd 2495 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( P  .\/  R )  =  ( R  .\/  S ) )
426, 41breqtrrd 4465 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( P  .\/  Q )  .<_  ( P 
.\/  R ) )
43423expia 1196 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( P  .\/  Q )  .<_  ( P  .\/  R ) ) )
4417, 10, 11hlatjcl 35507 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  P  e.  A  /\  R  e.  A )  ->  ( P  .\/  R
)  e.  ( Base `  K ) )
457, 8, 9, 44syl3anc 1226 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( P  .\/  R
)  e.  ( Base `  K ) )
4617, 26, 10latjle12 15894 . . . . . . . . . 10  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  Q  e.  ( Base `  K )  /\  ( P  .\/  R )  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  ( P  .\/  R )  /\  Q  .<_  ( P 
.\/  R ) )  <-> 
( P  .\/  Q
)  .<_  ( P  .\/  R ) ) )
4716, 19, 22, 45, 46syl13anc 1228 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .<_  ( P  .\/  R )  /\  Q  .<_  ( P 
.\/  R ) )  <-> 
( P  .\/  Q
)  .<_  ( P  .\/  R ) ) )
48 simpr 459 . . . . . . . . . 10  |-  ( ( P  .<_  ( P  .\/  R )  /\  Q  .<_  ( P  .\/  R
) )  ->  Q  .<_  ( P  .\/  R
) )
49 simp23 1029 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  P  =/=  Q )
5049necomd 2725 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  ->  Q  =/=  P )
5126, 10, 11hlatexchb1 35533 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( Q  e.  A  /\  R  e.  A  /\  P  e.  A
)  /\  Q  =/=  P )  ->  ( Q  .<_  ( P  .\/  R
)  <->  ( P  .\/  Q )  =  ( P 
.\/  R ) ) )
527, 20, 9, 8, 50, 51syl131anc 1239 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( Q  .<_  ( P 
.\/  R )  <->  ( P  .\/  Q )  =  ( P  .\/  R ) ) )
5348, 52syl5ib 219 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .<_  ( P  .\/  R )  /\  Q  .<_  ( P 
.\/  R ) )  ->  ( P  .\/  Q )  =  ( P 
.\/  R ) ) )
5447, 53sylbird 235 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( P  .\/  R )  ->  ( P  .\/  Q )  =  ( P  .\/  R
) ) )
5554adantr 463 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( ( P  .\/  Q )  .<_  ( P  .\/  R )  ->  ( P  .\/  Q )  =  ( P  .\/  R
) ) )
5643, 55syld 44 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( P  .\/  Q )  =  ( P  .\/  R
) ) )
57563impia 1191 . . . . 5  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( P  .\/  Q )  =  ( P  .\/  R ) )
5857, 41eqtrd 2495 . . . 4  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R  /\  ( P  .\/  Q )  .<_  ( R  .\/  S ) )  ->  ( P  .\/  Q )  =  ( R  .\/  S ) )
59583expia 1196 . . 3  |-  ( ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  /\  P  =/=  R )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( P  .\/  Q )  =  ( R  .\/  S
) ) )
6017, 10, 11hlatjcl 35507 . . . . . . 7  |-  ( ( K  e.  HL  /\  P  e.  A  /\  S  e.  A )  ->  ( P  .\/  S
)  e.  ( Base `  K ) )
617, 8, 23, 60syl3anc 1226 . . . . . 6  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( P  .\/  S
)  e.  ( Base `  K ) )
6217, 26, 10latjle12 15894 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  Q  e.  ( Base `  K )  /\  ( P  .\/  S )  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  ( P  .\/  S )  /\  Q  .<_  ( P 
.\/  S ) )  <-> 
( P  .\/  Q
)  .<_  ( P  .\/  S ) ) )
6316, 19, 22, 61, 62syl13anc 1228 . . . . 5  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .<_  ( P  .\/  S )  /\  Q  .<_  ( P 
.\/  S ) )  <-> 
( P  .\/  Q
)  .<_  ( P  .\/  S ) ) )
64 simpr 459 . . . . 5  |-  ( ( P  .<_  ( P  .\/  S )  /\  Q  .<_  ( P  .\/  S
) )  ->  Q  .<_  ( P  .\/  S
) )
6563, 64syl6bir 229 . . . 4  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( P  .\/  S )  ->  Q  .<_  ( P  .\/  S
) ) )
6626, 10, 11hlatexchb1 35533 . . . . 5  |-  ( ( K  e.  HL  /\  ( Q  e.  A  /\  S  e.  A  /\  P  e.  A
)  /\  Q  =/=  P )  ->  ( Q  .<_  ( P  .\/  S
)  <->  ( P  .\/  Q )  =  ( P 
.\/  S ) ) )
677, 20, 23, 8, 50, 66syl131anc 1239 . . . 4  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( Q  .<_  ( P 
.\/  S )  <->  ( P  .\/  Q )  =  ( P  .\/  S ) ) )
6865, 67sylibd 214 . . 3  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( P  .\/  S )  ->  ( P  .\/  Q )  =  ( P  .\/  S
) ) )
695, 59, 68pm2.61ne 2769 . 2  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  ->  ( P  .\/  Q )  =  ( R  .\/  S
) ) )
7017, 10, 11hlatjcl 35507 . . . . 5  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
717, 8, 20, 70syl3anc 1226 . . . 4  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( P  .\/  Q
)  e.  ( Base `  K ) )
7217, 26latref 15885 . . . 4  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
) )  ->  ( P  .\/  Q )  .<_  ( P  .\/  Q ) )
7316, 71, 72syl2anc 659 . . 3  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( P  .\/  Q
)  .<_  ( P  .\/  Q ) )
74 breq2 4443 . . 3  |-  ( ( P  .\/  Q )  =  ( R  .\/  S )  ->  ( ( P  .\/  Q )  .<_  ( P  .\/  Q )  <-> 
( P  .\/  Q
)  .<_  ( R  .\/  S ) ) )
7573, 74syl5ibcom 220 . 2  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  =  ( R 
.\/  S )  -> 
( P  .\/  Q
)  .<_  ( R  .\/  S ) ) )
7669, 75impbid 191 1  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( R  e.  A  /\  S  e.  A ) )  -> 
( ( P  .\/  Q )  .<_  ( R  .\/  S )  <->  ( P  .\/  Q )  =  ( R  .\/  S ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823    =/= wne 2649   class class class wbr 4439   ` cfv 5570  (class class class)co 6270   Basecbs 14719   lecple 14794   joincjn 15775   Latclat 15877   Atomscatm 35404   HLchlt 35491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-preset 15759  df-poset 15777  df-plt 15790  df-lub 15806  df-glb 15807  df-join 15808  df-meet 15809  df-p0 15871  df-lat 15878  df-covers 35407  df-ats 35408  df-atl 35439  df-cvlat 35463  df-hlat 35492
This theorem is referenced by:  2atjlej  35619  hlatexch3N  35620  hlatexch4  35621  2llnjaN  35706  dalem1  35799  lneq2at  35918  2llnma3r  35928  cdleme11c  36402  cdleme11  36411  cdleme35a  36590  cdleme42k  36626  cdlemg8b  36770  cdlemg13a  36793  cdlemg18b  36821  cdlemg42  36871  trljco  36882
  Copyright terms: Public domain W3C validator