Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemh.b |
|- B = ( Base ` K ) |
2 |
|
cdlemh.l |
|- .<_ = ( le ` K ) |
3 |
|
cdlemh.j |
|- .\/ = ( join ` K ) |
4 |
|
cdlemh.m |
|- ./\ = ( meet ` K ) |
5 |
|
cdlemh.a |
|- A = ( Atoms ` K ) |
6 |
|
cdlemh.h |
|- H = ( LHyp ` K ) |
7 |
|
cdlemh.t |
|- T = ( ( LTrn ` K ) ` W ) |
8 |
|
cdlemh.r |
|- R = ( ( trL ` K ) ` W ) |
9 |
|
cdlemh.s |
|- S = ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) ) |
10 |
|
cdlemh.z |
|- .0. = ( 0. ` K ) |
11 |
9
|
oveq1i |
|- ( S ./\ W ) = ( ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) ) ./\ W ) |
12 |
|
simp11l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> K e. HL ) |
13 |
|
hlol |
|- ( K e. HL -> K e. OL ) |
14 |
12 13
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> K e. OL ) |
15 |
12
|
hllatd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> K e. Lat ) |
16 |
|
simp2ll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> P e. A ) |
17 |
1 5
|
atbase |
|- ( P e. A -> P e. B ) |
18 |
16 17
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> P e. B ) |
19 |
|
simp11r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> W e. H ) |
20 |
12 19
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( K e. HL /\ W e. H ) ) |
21 |
|
simp13 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> G e. T ) |
22 |
1 6 7 8
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) e. B ) |
23 |
20 21 22
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` G ) e. B ) |
24 |
1 3
|
latjcl |
|- ( ( K e. Lat /\ P e. B /\ ( R ` G ) e. B ) -> ( P .\/ ( R ` G ) ) e. B ) |
25 |
15 18 23 24
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( P .\/ ( R ` G ) ) e. B ) |
26 |
|
simp2rl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> Q e. A ) |
27 |
1 5
|
atbase |
|- ( Q e. A -> Q e. B ) |
28 |
26 27
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> Q e. B ) |
29 |
|
simp12 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> F e. T ) |
30 |
6 7
|
ltrncnv |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T ) |
31 |
20 29 30
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> `' F e. T ) |
32 |
6 7
|
ltrnco |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ `' F e. T ) -> ( G o. `' F ) e. T ) |
33 |
20 21 31 32
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( G o. `' F ) e. T ) |
34 |
1 6 7 8
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G o. `' F ) e. T ) -> ( R ` ( G o. `' F ) ) e. B ) |
35 |
20 33 34
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` ( G o. `' F ) ) e. B ) |
36 |
1 3
|
latjcl |
|- ( ( K e. Lat /\ Q e. B /\ ( R ` ( G o. `' F ) ) e. B ) -> ( Q .\/ ( R ` ( G o. `' F ) ) ) e. B ) |
37 |
15 28 35 36
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( Q .\/ ( R ` ( G o. `' F ) ) ) e. B ) |
38 |
1 6
|
lhpbase |
|- ( W e. H -> W e. B ) |
39 |
19 38
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> W e. B ) |
40 |
1 4
|
latmassOLD |
|- ( ( K e. OL /\ ( ( P .\/ ( R ` G ) ) e. B /\ ( Q .\/ ( R ` ( G o. `' F ) ) ) e. B /\ W e. B ) ) -> ( ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) ) ./\ W ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q .\/ ( R ` ( G o. `' F ) ) ) ./\ W ) ) ) |
41 |
14 25 37 39 40
|
syl13anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) ) ./\ W ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q .\/ ( R ` ( G o. `' F ) ) ) ./\ W ) ) ) |
42 |
|
simp2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( Q e. A /\ -. Q .<_ W ) ) |
43 |
2 4 10 5 6
|
lhpmat |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ./\ W ) = .0. ) |
44 |
20 42 43
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( Q ./\ W ) = .0. ) |
45 |
44
|
oveq1d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( Q ./\ W ) .\/ ( R ` ( G o. `' F ) ) ) = ( .0. .\/ ( R ` ( G o. `' F ) ) ) ) |
46 |
2 6 7 8
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G o. `' F ) e. T ) -> ( R ` ( G o. `' F ) ) .<_ W ) |
47 |
20 33 46
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` ( G o. `' F ) ) .<_ W ) |
48 |
1 2 3 4 5
|
atmod4i2 |
|- ( ( K e. HL /\ ( Q e. A /\ ( R ` ( G o. `' F ) ) e. B /\ W e. B ) /\ ( R ` ( G o. `' F ) ) .<_ W ) -> ( ( Q ./\ W ) .\/ ( R ` ( G o. `' F ) ) ) = ( ( Q .\/ ( R ` ( G o. `' F ) ) ) ./\ W ) ) |
49 |
12 26 35 39 47 48
|
syl131anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( Q ./\ W ) .\/ ( R ` ( G o. `' F ) ) ) = ( ( Q .\/ ( R ` ( G o. `' F ) ) ) ./\ W ) ) |
50 |
1 3 10
|
olj02 |
|- ( ( K e. OL /\ ( R ` ( G o. `' F ) ) e. B ) -> ( .0. .\/ ( R ` ( G o. `' F ) ) ) = ( R ` ( G o. `' F ) ) ) |
51 |
14 35 50
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( .0. .\/ ( R ` ( G o. `' F ) ) ) = ( R ` ( G o. `' F ) ) ) |
52 |
45 49 51
|
3eqtr3rd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` ( G o. `' F ) ) = ( ( Q .\/ ( R ` ( G o. `' F ) ) ) ./\ W ) ) |
53 |
52
|
oveq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( P .\/ ( R ` G ) ) ./\ ( R ` ( G o. `' F ) ) ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q .\/ ( R ` ( G o. `' F ) ) ) ./\ W ) ) ) |
54 |
|
simp2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( P e. A /\ -. P .<_ W ) ) |
55 |
21 31
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( G e. T /\ `' F e. T ) ) |
56 |
|
simp33 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` F ) =/= ( R ` G ) ) |
57 |
56
|
necomd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` G ) =/= ( R ` F ) ) |
58 |
6 7 8
|
trlcnv |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) ) |
59 |
20 29 58
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` `' F ) = ( R ` F ) ) |
60 |
57 59
|
neeqtrrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` G ) =/= ( R ` `' F ) ) |
61 |
|
simp31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> F =/= ( _I |` B ) ) |
62 |
1 6 7
|
ltrncnvnid |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> `' F =/= ( _I |` B ) ) |
63 |
20 29 61 62
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> `' F =/= ( _I |` B ) ) |
64 |
1 6 7 8
|
trlcone |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ `' F e. T ) /\ ( ( R ` G ) =/= ( R ` `' F ) /\ `' F =/= ( _I |` B ) ) ) -> ( R ` G ) =/= ( R ` ( G o. `' F ) ) ) |
65 |
20 55 60 63 64
|
syl112anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` G ) =/= ( R ` ( G o. `' F ) ) ) |
66 |
|
simp32 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> G =/= ( _I |` B ) ) |
67 |
1 5 6 7 8
|
trlnidat |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ G =/= ( _I |` B ) ) -> ( R ` G ) e. A ) |
68 |
20 21 66 67
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` G ) e. A ) |
69 |
2 6 7 8
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) .<_ W ) |
70 |
20 21 69
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` G ) .<_ W ) |
71 |
5 6 7 8
|
trlcoat |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ `' F e. T ) /\ ( R ` G ) =/= ( R ` `' F ) ) -> ( R ` ( G o. `' F ) ) e. A ) |
72 |
20 55 60 71
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` ( G o. `' F ) ) e. A ) |
73 |
2 3 4 10 5 6
|
lhp2at0 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` G ) =/= ( R ` ( G o. `' F ) ) ) /\ ( ( R ` G ) e. A /\ ( R ` G ) .<_ W ) /\ ( ( R ` ( G o. `' F ) ) e. A /\ ( R ` ( G o. `' F ) ) .<_ W ) ) -> ( ( P .\/ ( R ` G ) ) ./\ ( R ` ( G o. `' F ) ) ) = .0. ) |
74 |
20 54 65 68 70 72 47 73
|
syl322anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( P .\/ ( R ` G ) ) ./\ ( R ` ( G o. `' F ) ) ) = .0. ) |
75 |
41 53 74
|
3eqtr2rd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> .0. = ( ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) ) ./\ W ) ) |
76 |
11 75
|
eqtr4id |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( S ./\ W ) = .0. ) |