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

Theorem dalem54 33209
Description: Lemma for dath 33219. Line  G H intersects the auxiliary axis of perspectivity  B. (Contributed by NM, 8-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph  |-  ( ph  <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A
) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  ( ( -.  C  .<_  ( P  .\/  Q
)  /\  -.  C  .<_  ( Q  .\/  R
)  /\  -.  C  .<_  ( R  .\/  P
) )  /\  ( -.  C  .<_  ( S 
.\/  T )  /\  -.  C  .<_  ( T 
.\/  U )  /\  -.  C  .<_  ( U 
.\/  S ) )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
.\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )
dalem.l  |-  .<_  =  ( le `  K )
dalem.j  |-  .\/  =  ( join `  K )
dalem.a  |-  A  =  ( Atoms `  K )
dalem.ps  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
dalem54.m  |-  ./\  =  ( meet `  K )
dalem54.o  |-  O  =  ( LPlanes `  K )
dalem54.y  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
dalem54.z  |-  Z  =  ( ( S  .\/  T )  .\/  U )
dalem54.g  |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )
dalem54.h  |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )
dalem54.i  |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )
dalem54.b1  |-  B  =  ( ( ( G 
.\/  H )  .\/  I )  ./\  Y
)
Assertion
Ref Expression
dalem54  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  B )  e.  A )

Proof of Theorem dalem54
StepHypRef Expression
1 dalem.ph . . . 4  |-  ( ph  <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A
) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  ( ( -.  C  .<_  ( P  .\/  Q
)  /\  -.  C  .<_  ( Q  .\/  R
)  /\  -.  C  .<_  ( R  .\/  P
) )  /\  ( -.  C  .<_  ( S 
.\/  T )  /\  -.  C  .<_  ( T 
.\/  U )  /\  -.  C  .<_  ( U 
.\/  S ) )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
.\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )
21dalemkehl 33106 . . 3  |-  ( ph  ->  K  e.  HL )
323ad2ant1 1026 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  HL )
4 dalem.l . . . 4  |-  .<_  =  ( le `  K )
5 dalem.j . . . 4  |-  .\/  =  ( join `  K )
6 dalem.a . . . 4  |-  A  =  ( Atoms `  K )
7 dalem.ps . . . 4  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
8 dalem54.m . . . 4  |-  ./\  =  ( meet `  K )
9 dalem54.o . . . 4  |-  O  =  ( LPlanes `  K )
10 dalem54.y . . . 4  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
11 dalem54.z . . . 4  |-  Z  =  ( ( S  .\/  T )  .\/  U )
12 dalem54.g . . . 4  |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )
131, 4, 5, 6, 7, 8, 9, 10, 11, 12dalem23 33179 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  G  e.  A )
14 dalem54.h . . . 4  |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )
151, 4, 5, 6, 7, 8, 9, 10, 11, 14dalem29 33184 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  H  e.  A )
16 dalem54.i . . . 4  |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )
171, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 16dalem41 33196 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  G  =/=  H )
18 eqid 2422 . . . 4  |-  ( LLines `  K )  =  (
LLines `  K )
195, 6, 18llni2 32995 . . 3  |-  ( ( ( K  e.  HL  /\  G  e.  A  /\  H  e.  A )  /\  G  =/=  H
)  ->  ( G  .\/  H )  e.  (
LLines `  K ) )
203, 13, 15, 17, 19syl31anc 1267 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( G  .\/  H
)  e.  ( LLines `  K ) )
21 dalem54.b1 . . 3  |-  B  =  ( ( ( G 
.\/  H )  .\/  I )  ./\  Y
)
221, 4, 5, 6, 7, 8, 18, 9, 10, 11, 12, 14, 16, 21dalem53 33208 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  B  e.  ( LLines `  K ) )
231dalemkelat 33107 . . . . . . 7  |-  ( ph  ->  K  e.  Lat )
24233ad2ant1 1026 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  Lat )
25 eqid 2422 . . . . . . . . 9  |-  ( Base `  K )  =  (
Base `  K )
2625, 18llnbase 32992 . . . . . . . 8  |-  ( ( G  .\/  H )  e.  ( LLines `  K
)  ->  ( G  .\/  H )  e.  (
Base `  K )
)
2720, 26syl 17 . . . . . . 7  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( G  .\/  H
)  e.  ( Base `  K ) )
281, 4, 5, 6, 7, 8, 9, 10, 11, 16dalem34 33189 . . . . . . . 8  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  I  e.  A )
2925, 6atbase 32773 . . . . . . . 8  |-  ( I  e.  A  ->  I  e.  ( Base `  K
) )
3028, 29syl 17 . . . . . . 7  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  I  e.  ( Base `  K ) )
3125, 5latjcl 16284 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( G  .\/  H )  e.  ( Base `  K
)  /\  I  e.  ( Base `  K )
)  ->  ( ( G  .\/  H )  .\/  I )  e.  (
Base `  K )
)
3224, 27, 30, 31syl3anc 1264 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  .\/  I )  e.  ( Base `  K
) )
331, 9dalemyeb 33132 . . . . . . 7  |-  ( ph  ->  Y  e.  ( Base `  K ) )
34333ad2ant1 1026 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  Y  e.  ( Base `  K ) )
3525, 4, 8latmle2 16310 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( G  .\/  H )  .\/  I )  e.  ( Base `  K
)  /\  Y  e.  ( Base `  K )
)  ->  ( (
( G  .\/  H
)  .\/  I )  ./\  Y )  .<_  Y )
3624, 32, 34, 35syl3anc 1264 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( ( G 
.\/  H )  .\/  I )  ./\  Y
)  .<_  Y )
3721, 36syl5eqbr 4454 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  B  .<_  Y )
381, 4, 5, 6, 7, 8, 9, 10, 11, 12dalem24 33180 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  G  .<_  Y )
3925, 6atbase 32773 . . . . . . . 8  |-  ( G  e.  A  ->  G  e.  ( Base `  K
) )
4013, 39syl 17 . . . . . . 7  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  G  e.  ( Base `  K ) )
4125, 6atbase 32773 . . . . . . . 8  |-  ( H  e.  A  ->  H  e.  ( Base `  K
) )
4215, 41syl 17 . . . . . . 7  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  H  e.  ( Base `  K ) )
4325, 4, 5latjle12 16295 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( G  e.  ( Base `  K )  /\  H  e.  ( Base `  K )  /\  Y  e.  ( Base `  K
) ) )  -> 
( ( G  .<_  Y  /\  H  .<_  Y )  <-> 
( G  .\/  H
)  .<_  Y ) )
4424, 40, 42, 34, 43syl13anc 1266 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .<_  Y  /\  H  .<_  Y )  <-> 
( G  .\/  H
)  .<_  Y ) )
45 simpl 458 . . . . . 6  |-  ( ( G  .<_  Y  /\  H  .<_  Y )  ->  G  .<_  Y )
4644, 45syl6bir 232 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  .<_  Y  ->  G 
.<_  Y ) )
4738, 46mtod 180 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  ( G  .\/  H
)  .<_  Y )
48 nbrne2 4439 . . . 4  |-  ( ( B  .<_  Y  /\  -.  ( G  .\/  H
)  .<_  Y )  ->  B  =/=  ( G  .\/  H ) )
4937, 47, 48syl2anc 665 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  B  =/=  ( G  .\/  H ) )
5049necomd 2695 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( G  .\/  H
)  =/=  B )
51 hlatl 32844 . . . 4  |-  ( K  e.  HL  ->  K  e.  AtLat )
523, 51syl 17 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  AtLat )
5325, 18llnbase 32992 . . . . 5  |-  ( B  e.  ( LLines `  K
)  ->  B  e.  ( Base `  K )
)
5422, 53syl 17 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  B  e.  ( Base `  K ) )
5525, 8latmcl 16285 . . . 4  |-  ( ( K  e.  Lat  /\  ( G  .\/  H )  e.  ( Base `  K
)  /\  B  e.  ( Base `  K )
)  ->  ( ( G  .\/  H )  ./\  B )  e.  ( Base `  K ) )
5624, 27, 54, 55syl3anc 1264 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  B )  e.  ( Base `  K
) )
571, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 16dalem52 33207 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  e.  A )
581, 5, 6dalempjqeb 33128 . . . . . 6  |-  ( ph  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
59583ad2ant1 1026 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( P  .\/  Q
)  e.  ( Base `  K ) )
6025, 4, 8latmle1 16309 . . . . 5  |-  ( ( K  e.  Lat  /\  ( G  .\/  H )  e.  ( Base `  K
)  /\  ( P  .\/  Q )  e.  (
Base `  K )
)  ->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( G  .\/  H ) )
6124, 27, 59, 60syl3anc 1264 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( G  .\/  H ) )
621, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 16dalem51 33206 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( ( ( K  e.  HL  /\  c  e.  A )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A
)  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) )  /\  ( ( ( G 
.\/  H )  .\/  I )  e.  O  /\  Y  e.  O
)  /\  ( ( -.  c  .<_  ( G 
.\/  H )  /\  -.  c  .<_  ( H 
.\/  I )  /\  -.  c  .<_  ( I 
.\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q
)  /\  -.  c  .<_  ( Q  .\/  R
)  /\  -.  c  .<_  ( R  .\/  P
) )  /\  (
c  .<_  ( G  .\/  P )  /\  c  .<_  ( H  .\/  Q )  /\  c  .<_  ( I 
.\/  R ) ) ) )  /\  (
( G  .\/  H
)  .\/  I )  =/=  Y ) )
6362simpld 460 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( ( K  e.  HL  /\  c  e.  A )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A
) )  /\  (
( ( G  .\/  H )  .\/  I )  e.  O  /\  Y  e.  O )  /\  (
( -.  c  .<_  ( G  .\/  H )  /\  -.  c  .<_  ( H  .\/  I )  /\  -.  c  .<_  ( I  .\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q )  /\  -.  c  .<_  ( Q  .\/  R )  /\  -.  c  .<_  ( R  .\/  P
) )  /\  (
c  .<_  ( G  .\/  P )  /\  c  .<_  ( H  .\/  Q )  /\  c  .<_  ( I 
.\/  R ) ) ) ) )
6425, 6atbase 32773 . . . . . . . 8  |-  ( c  e.  A  ->  c  e.  ( Base `  K
) )
6564anim2i 571 . . . . . . 7  |-  ( ( K  e.  HL  /\  c  e.  A )  ->  ( K  e.  HL  /\  c  e.  ( Base `  K ) ) )
66653anim1i 1191 . . . . . 6  |-  ( ( ( K  e.  HL  /\  c  e.  A )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )
)  ->  ( ( K  e.  HL  /\  c  e.  ( Base `  K
) )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A
) ) )
67 biid 239 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  c  e.  ( Base `  K
) )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A
) )  /\  (
( ( G  .\/  H )  .\/  I )  e.  O  /\  Y  e.  O )  /\  (
( -.  c  .<_  ( G  .\/  H )  /\  -.  c  .<_  ( H  .\/  I )  /\  -.  c  .<_  ( I  .\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q )  /\  -.  c  .<_  ( Q  .\/  R )  /\  -.  c  .<_  ( R  .\/  P
) )  /\  (
c  .<_  ( G  .\/  P )  /\  c  .<_  ( H  .\/  Q )  /\  c  .<_  ( I 
.\/  R ) ) ) )  <->  ( (
( K  e.  HL  /\  c  e.  ( Base `  K ) )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A
)  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) )  /\  ( ( ( G 
.\/  H )  .\/  I )  e.  O  /\  Y  e.  O
)  /\  ( ( -.  c  .<_  ( G 
.\/  H )  /\  -.  c  .<_  ( H 
.\/  I )  /\  -.  c  .<_  ( I 
.\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q
)  /\  -.  c  .<_  ( Q  .\/  R
)  /\  -.  c  .<_  ( R  .\/  P
) )  /\  (
c  .<_  ( G  .\/  P )  /\  c  .<_  ( H  .\/  Q )  /\  c  .<_  ( I 
.\/  R ) ) ) ) )
68 eqid 2422 . . . . . . 7  |-  ( ( G  .\/  H ) 
.\/  I )  =  ( ( G  .\/  H )  .\/  I )
69 eqid 2422 . . . . . . 7  |-  ( ( G  .\/  H ) 
./\  ( P  .\/  Q ) )  =  ( ( G  .\/  H
)  ./\  ( P  .\/  Q ) )
7067, 4, 5, 6, 8, 9, 68, 10, 21, 69dalem10 33156 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  c  e.  ( Base `  K
) )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A
) )  /\  (
( ( G  .\/  H )  .\/  I )  e.  O  /\  Y  e.  O )  /\  (
( -.  c  .<_  ( G  .\/  H )  /\  -.  c  .<_  ( H  .\/  I )  /\  -.  c  .<_  ( I  .\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q )  /\  -.  c  .<_  ( Q  .\/  R )  /\  -.  c  .<_  ( R  .\/  P
) )  /\  (
c  .<_  ( G  .\/  P )  /\  c  .<_  ( H  .\/  Q )  /\  c  .<_  ( I 
.\/  R ) ) ) )  ->  (
( G  .\/  H
)  ./\  ( P  .\/  Q ) )  .<_  B )
7166, 70syl3an1 1297 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  c  e.  A )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A
) )  /\  (
( ( G  .\/  H )  .\/  I )  e.  O  /\  Y  e.  O )  /\  (
( -.  c  .<_  ( G  .\/  H )  /\  -.  c  .<_  ( H  .\/  I )  /\  -.  c  .<_  ( I  .\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q )  /\  -.  c  .<_  ( Q  .\/  R )  /\  -.  c  .<_  ( R  .\/  P
) )  /\  (
c  .<_  ( G  .\/  P )  /\  c  .<_  ( H  .\/  Q )  /\  c  .<_  ( I 
.\/  R ) ) ) )  ->  (
( G  .\/  H
)  ./\  ( P  .\/  Q ) )  .<_  B )
7263, 71syl 17 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  B )
7325, 8latmcl 16285 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( G  .\/  H )  e.  ( Base `  K
)  /\  ( P  .\/  Q )  e.  (
Base `  K )
)  ->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  e.  ( Base `  K ) )
7424, 27, 59, 73syl3anc 1264 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  e.  ( Base `  K
) )
7525, 4, 8latlem12 16311 . . . . 5  |-  ( ( K  e.  Lat  /\  ( ( ( G 
.\/  H )  ./\  ( P  .\/  Q ) )  e.  ( Base `  K )  /\  ( G  .\/  H )  e.  ( Base `  K
)  /\  B  e.  ( Base `  K )
) )  ->  (
( ( ( G 
.\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( G  .\/  H )  /\  (
( G  .\/  H
)  ./\  ( P  .\/  Q ) )  .<_  B )  <->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( ( G  .\/  H )  ./\  B ) ) )
7624, 74, 27, 54, 75syl13anc 1266 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( ( ( G  .\/  H ) 
./\  ( P  .\/  Q ) )  .<_  ( G 
.\/  H )  /\  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  B )  <->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( ( G  .\/  H )  ./\  B ) ) )
7761, 72, 76mpbi2and 929 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( ( G  .\/  H )  ./\  B )
)
78 eqid 2422 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
7925, 4, 78, 6atlen0 32794 . . 3  |-  ( ( ( K  e.  AtLat  /\  ( ( G  .\/  H )  ./\  B )  e.  ( Base `  K
)  /\  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  e.  A )  /\  ( ( G 
.\/  H )  ./\  ( P  .\/  Q ) )  .<_  ( ( G  .\/  H )  ./\  B ) )  ->  (
( G  .\/  H
)  ./\  B )  =/=  ( 0. `  K
) )
8052, 56, 57, 77, 79syl31anc 1267 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  B )  =/=  ( 0. `  K
) )
818, 78, 6, 182llnmat 33007 . 2  |-  ( ( ( K  e.  HL  /\  ( G  .\/  H
)  e.  ( LLines `  K )  /\  B  e.  ( LLines `  K )
)  /\  ( ( G  .\/  H )  =/= 
B  /\  ( ( G  .\/  H )  ./\  B )  =/=  ( 0.
`  K ) ) )  ->  ( ( G  .\/  H )  ./\  B )  e.  A )
823, 20, 22, 50, 80, 81syl32anc 1272 1  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( G  .\/  H )  ./\  B )  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868    =/= wne 2618   class class class wbr 4420   ` cfv 5597  (class class class)co 6301   Basecbs 15108   lecple 15184   joincjn 16176   meetcmee 16177   0.cp0 16270   Latclat 16278   Atomscatm 32747   AtLatcal 32748   HLchlt 32834   LLinesclln 32974   LPlanesclpl 32975
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 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593
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 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-preset 16160  df-poset 16178  df-plt 16191  df-lub 16207  df-glb 16208  df-join 16209  df-meet 16210  df-p0 16272  df-lat 16279  df-clat 16341  df-oposet 32660  df-ol 32662  df-oml 32663  df-covers 32750  df-ats 32751  df-atl 32782  df-cvlat 32806  df-hlat 32835  df-llines 32981  df-lplanes 32982  df-lvols 32983
This theorem is referenced by:  dalem55  33210  dalem57  33212
  Copyright terms: Public domain W3C validator