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

Metamath Proof Explorer

Theorem cdlemkid1

Description: Lemma for cdlemkid . (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b 
|- B = ( Base ` K )
cdlemk5.l 
|- .<_ = ( le ` K )
cdlemk5.j 
|- .\/ = ( join ` K )
cdlemk5.m 
|- ./\ = ( meet ` K )
cdlemk5.a 
|- A = ( Atoms ` K )
cdlemk5.h 
|- H = ( LHyp ` K )
cdlemk5.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemk5.r 
|- R = ( ( trL ` K ) ` W )
cdlemk5.z 
|- Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
Assertion cdlemkid1 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( Z .\/ ( R ` b ) ) = ( P .\/ ( R ` b ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk5.b 
 |-  B = ( Base ` K )
2 cdlemk5.l 
 |-  .<_ = ( le ` K )
3 cdlemk5.j 
 |-  .\/ = ( join ` K )
4 cdlemk5.m 
 |-  ./\ = ( meet ` K )
5 cdlemk5.a 
 |-  A = ( Atoms ` K )
6 cdlemk5.h 
 |-  H = ( LHyp ` K )
7 cdlemk5.t 
 |-  T = ( ( LTrn ` K ) ` W )
8 cdlemk5.r 
 |-  R = ( ( trL ` K ) ` W )
9 cdlemk5.z 
 |-  Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
10 9 oveq1i 
 |-  ( Z .\/ ( R ` b ) ) = ( ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) ) .\/ ( R ` b ) )
11 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> K e. HL )
12 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( K e. HL /\ W e. H ) )
13 simp3rl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> b e. T )
14 simp3rr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> b =/= ( _I |` B ) )
15 1 5 6 7 8 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ b e. T /\ b =/= ( _I |` B ) ) -> ( R ` b ) e. A )
16 12 13 14 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` b ) e. A )
17 simp3ll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> P e. A )
18 1 3 5 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ ( R ` b ) e. A ) -> ( P .\/ ( R ` b ) ) e. B )
19 11 17 16 18 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( P .\/ ( R ` b ) ) e. B )
20 11 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> K e. Lat )
21 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> N e. T )
22 1 5 atbase 
 |-  ( P e. A -> P e. B )
23 17 22 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> P e. B )
24 1 6 7 ltrncl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ N e. T /\ P e. B ) -> ( N ` P ) e. B )
25 12 21 23 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( N ` P ) e. B )
26 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> F e. T )
27 6 7 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
28 12 26 27 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> `' F e. T )
29 6 7 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ b e. T /\ `' F e. T ) -> ( b o. `' F ) e. T )
30 12 13 28 29 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( b o. `' F ) e. T )
31 1 6 7 8 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( b o. `' F ) e. T ) -> ( R ` ( b o. `' F ) ) e. B )
32 12 30 31 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` ( b o. `' F ) ) e. B )
33 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( N ` P ) e. B /\ ( R ` ( b o. `' F ) ) e. B ) -> ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) e. B )
34 20 25 32 33 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) e. B )
35 2 3 5 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ ( R ` b ) e. A ) -> ( R ` b ) .<_ ( P .\/ ( R ` b ) ) )
36 11 17 16 35 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` b ) .<_ ( P .\/ ( R ` b ) ) )
37 1 2 3 4 5 atmod2i1 
 |-  ( ( K e. HL /\ ( ( R ` b ) e. A /\ ( P .\/ ( R ` b ) ) e. B /\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) e. B ) /\ ( R ` b ) .<_ ( P .\/ ( R ` b ) ) ) -> ( ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) ) .\/ ( R ` b ) ) = ( ( P .\/ ( R ` b ) ) ./\ ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) ) )
38 11 16 19 34 36 37 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) ) .\/ ( R ` b ) ) = ( ( P .\/ ( R ` b ) ) ./\ ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) ) )
39 1 5 atbase 
 |-  ( ( R ` b ) e. A -> ( R ` b ) e. B )
40 16 39 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` b ) e. B )
41 1 6 7 8 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ N e. T ) -> ( R ` N ) e. B )
42 12 21 41 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` N ) e. B )
43 1 3 latj32 
 |-  ( ( K e. Lat /\ ( P e. B /\ ( R ` b ) e. B /\ ( R ` N ) e. B ) ) -> ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) = ( ( P .\/ ( R ` N ) ) .\/ ( R ` b ) ) )
44 20 23 40 42 43 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) = ( ( P .\/ ( R ` N ) ) .\/ ( R ` b ) ) )
45 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
46 2 3 5 6 7 8 trljat3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ N e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` N ) ) = ( ( N ` P ) .\/ ( R ` N ) ) )
47 12 21 45 46 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( P .\/ ( R ` N ) ) = ( ( N ` P ) .\/ ( R ` N ) ) )
48 47 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( P .\/ ( R ` N ) ) .\/ ( R ` b ) ) = ( ( ( N ` P ) .\/ ( R ` N ) ) .\/ ( R ` b ) ) )
49 1 3 latjass 
 |-  ( ( K e. Lat /\ ( ( N ` P ) e. B /\ ( R ` N ) e. B /\ ( R ` b ) e. B ) ) -> ( ( ( N ` P ) .\/ ( R ` N ) ) .\/ ( R ` b ) ) = ( ( N ` P ) .\/ ( ( R ` N ) .\/ ( R ` b ) ) ) )
50 20 25 42 40 49 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( ( N ` P ) .\/ ( R ` N ) ) .\/ ( R ` b ) ) = ( ( N ` P ) .\/ ( ( R ` N ) .\/ ( R ` b ) ) ) )
51 44 48 50 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) = ( ( N ` P ) .\/ ( ( R ` N ) .\/ ( R ` b ) ) ) )
52 1 3 latjass 
 |-  ( ( K e. Lat /\ ( ( N ` P ) e. B /\ ( R ` ( b o. `' F ) ) e. B /\ ( R ` b ) e. B ) ) -> ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) = ( ( N ` P ) .\/ ( ( R ` ( b o. `' F ) ) .\/ ( R ` b ) ) ) )
53 20 25 32 40 52 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) = ( ( N ` P ) .\/ ( ( R ` ( b o. `' F ) ) .\/ ( R ` b ) ) ) )
54 1 3 latjcom 
 |-  ( ( K e. Lat /\ ( R ` N ) e. B /\ ( R ` b ) e. B ) -> ( ( R ` N ) .\/ ( R ` b ) ) = ( ( R ` b ) .\/ ( R ` N ) ) )
55 20 42 40 54 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( R ` N ) .\/ ( R ` b ) ) = ( ( R ` b ) .\/ ( R ` N ) ) )
56 6 7 8 trlcnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) )
57 12 26 56 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` `' F ) = ( R ` F ) )
58 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` F ) = ( R ` N ) )
59 57 58 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( R ` `' F ) = ( R ` N ) )
60 59 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( R ` b ) .\/ ( R ` `' F ) ) = ( ( R ` b ) .\/ ( R ` N ) ) )
61 55 60 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( R ` N ) .\/ ( R ` b ) ) = ( ( R ` b ) .\/ ( R ` `' F ) ) )
62 3 6 7 8 trljco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ b e. T /\ `' F e. T ) -> ( ( R ` b ) .\/ ( R ` ( b o. `' F ) ) ) = ( ( R ` b ) .\/ ( R ` `' F ) ) )
63 12 13 28 62 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( R ` b ) .\/ ( R ` ( b o. `' F ) ) ) = ( ( R ` b ) .\/ ( R ` `' F ) ) )
64 1 3 latjcom 
 |-  ( ( K e. Lat /\ ( R ` b ) e. B /\ ( R ` ( b o. `' F ) ) e. B ) -> ( ( R ` b ) .\/ ( R ` ( b o. `' F ) ) ) = ( ( R ` ( b o. `' F ) ) .\/ ( R ` b ) ) )
65 20 40 32 64 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( R ` b ) .\/ ( R ` ( b o. `' F ) ) ) = ( ( R ` ( b o. `' F ) ) .\/ ( R ` b ) ) )
66 61 63 65 3eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( R ` N ) .\/ ( R ` b ) ) = ( ( R ` ( b o. `' F ) ) .\/ ( R ` b ) ) )
67 66 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( N ` P ) .\/ ( ( R ` N ) .\/ ( R ` b ) ) ) = ( ( N ` P ) .\/ ( ( R ` ( b o. `' F ) ) .\/ ( R ` b ) ) ) )
68 53 67 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) = ( ( N ` P ) .\/ ( ( R ` N ) .\/ ( R ` b ) ) ) )
69 51 68 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) = ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) )
70 69 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( P .\/ ( R ` b ) ) ./\ ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) ) = ( ( P .\/ ( R ` b ) ) ./\ ( ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) .\/ ( R ` b ) ) ) )
71 1 3 4 latabs2 
 |-  ( ( K e. Lat /\ ( P .\/ ( R ` b ) ) e. B /\ ( R ` N ) e. B ) -> ( ( P .\/ ( R ` b ) ) ./\ ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) ) = ( P .\/ ( R ` b ) ) )
72 20 19 42 71 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( P .\/ ( R ` b ) ) ./\ ( ( P .\/ ( R ` b ) ) .\/ ( R ` N ) ) ) = ( P .\/ ( R ` b ) ) )
73 38 70 72 3eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) ) .\/ ( R ` b ) ) = ( P .\/ ( R ` b ) ) )
74 10 73 eqtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( b e. T /\ b =/= ( _I |` B ) ) ) ) -> ( Z .\/ ( R ` b ) ) = ( P .\/ ( R ` b ) ) )