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

Metamath Proof Explorer

Theorem cdleme32fva

Description: Part of proof of Lemma D in Crawley p. 113. Value of F at an atom not under W . (Contributed by NM, 2-Mar-2013)

Ref Expression
Hypotheses cdleme32.b 
|- B = ( Base ` K )
cdleme32.l 
|- .<_ = ( le ` K )
cdleme32.j 
|- .\/ = ( join ` K )
cdleme32.m 
|- ./\ = ( meet ` K )
cdleme32.a 
|- A = ( Atoms ` K )
cdleme32.h 
|- H = ( LHyp ` K )
cdleme32.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme32.c 
|- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme32.d 
|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme32.e 
|- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) )
cdleme32.i 
|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) )
cdleme32.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , C )
cdleme32.o 
|- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
cdleme32.f 
|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
Assertion cdleme32fva 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> [_ R / x ]_ O = [_ R / s ]_ N )

Proof

Step Hyp Ref Expression
1 cdleme32.b 
 |-  B = ( Base ` K )
2 cdleme32.l 
 |-  .<_ = ( le ` K )
3 cdleme32.j 
 |-  .\/ = ( join ` K )
4 cdleme32.m 
 |-  ./\ = ( meet ` K )
5 cdleme32.a 
 |-  A = ( Atoms ` K )
6 cdleme32.h 
 |-  H = ( LHyp ` K )
7 cdleme32.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
8 cdleme32.c 
 |-  C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
9 cdleme32.d 
 |-  D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
10 cdleme32.e 
 |-  E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) )
11 cdleme32.i 
 |-  I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) )
12 cdleme32.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , C )
13 cdleme32.o 
 |-  O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
14 cdleme32.f 
 |-  F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
15 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> R e. A )
16 1 5 atbase 
 |-  ( R e. A -> R e. B )
17 15 16 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> R e. B )
18 eqid 
 |-  ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) )
19 13 18 cdleme31so 
 |-  ( R e. B -> [_ R / x ]_ O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) )
20 17 19 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> [_ R / x ]_ O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) )
21 simp1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
22 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> P =/= Q )
23 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( R e. A /\ -. R .<_ W ) )
24 1 2 3 4 5 6 7 8 9 10 11 12 cdleme32snb 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) ) -> [_ R / s ]_ N e. B )
25 21 22 23 24 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> [_ R / s ]_ N e. B )
26 nfv 
 |-  F/ s -. R .<_ W
27 nfcsb1v 
 |-  F/_ s [_ R / s ]_ N
28 27 nfeq2 
 |-  F/ s z = [_ R / s ]_ N
29 26 28 nfim 
 |-  F/ s ( -. R .<_ W -> z = [_ R / s ]_ N )
30 breq1 
 |-  ( s = R -> ( s .<_ W <-> R .<_ W ) )
31 30 notbid 
 |-  ( s = R -> ( -. s .<_ W <-> -. R .<_ W ) )
32 csbeq1a 
 |-  ( s = R -> N = [_ R / s ]_ N )
33 32 eqeq2d 
 |-  ( s = R -> ( z = N <-> z = [_ R / s ]_ N ) )
34 31 33 imbi12d 
 |-  ( s = R -> ( ( -. s .<_ W -> z = N ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
35 34 ax-gen 
 |-  A. s ( s = R -> ( ( -. s .<_ W -> z = N ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
36 ceqsralt 
 |-  ( ( F/ s ( -. R .<_ W -> z = [_ R / s ]_ N ) /\ A. s ( s = R -> ( ( -. s .<_ W -> z = N ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) ) /\ R e. A ) -> ( A. s e. A ( s = R -> ( -. s .<_ W -> z = N ) ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
37 29 35 36 mp3an12 
 |-  ( R e. A -> ( A. s e. A ( s = R -> ( -. s .<_ W -> z = N ) ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
38 37 adantr 
 |-  ( ( R e. A /\ -. R .<_ W ) -> ( A. s e. A ( s = R -> ( -. s .<_ W -> z = N ) ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
39 38 3ad2ant2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( A. s e. A ( s = R -> ( -. s .<_ W -> z = N ) ) <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
40 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( K e. HL /\ W e. H ) )
41 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
42 2 4 41 5 6 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
43 40 23 42 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( R ./\ W ) = ( 0. ` K ) )
44 43 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
45 44 oveq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( s .\/ ( R ./\ W ) ) = ( s .\/ ( 0. ` K ) ) )
46 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> K e. HL )
47 46 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> K e. HL )
48 hlol 
 |-  ( K e. HL -> K e. OL )
49 47 48 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> K e. OL )
50 1 5 atbase 
 |-  ( s e. A -> s e. B )
51 50 ad2antrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> s e. B )
52 1 3 41 olj01 
 |-  ( ( K e. OL /\ s e. B ) -> ( s .\/ ( 0. ` K ) ) = s )
53 49 51 52 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( s .\/ ( 0. ` K ) ) = s )
54 45 53 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( s .\/ ( R ./\ W ) ) = s )
55 54 eqeq1d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( ( s .\/ ( R ./\ W ) ) = R <-> s = R ) )
56 44 oveq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( N .\/ ( R ./\ W ) ) = ( N .\/ ( 0. ` K ) ) )
57 simpl11 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( K e. HL /\ W e. H ) )
58 simpl12 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) )
59 simpl13 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
60 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( s e. A /\ -. s .<_ W ) )
61 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> P =/= Q )
62 1 2 3 4 5 6 7 8 9 10 11 12 cdleme27cl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( s e. A /\ -. s .<_ W ) /\ P =/= Q ) ) -> N e. B )
63 57 58 59 60 61 62 syl122anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> N e. B )
64 1 3 41 olj01 
 |-  ( ( K e. OL /\ N e. B ) -> ( N .\/ ( 0. ` K ) ) = N )
65 49 63 64 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( N .\/ ( 0. ` K ) ) = N )
66 56 65 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( N .\/ ( R ./\ W ) ) = N )
67 66 eqeq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( z = ( N .\/ ( R ./\ W ) ) <-> z = N ) )
68 55 67 imbi12d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( s = R -> z = N ) ) )
69 68 expr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ s e. A ) -> ( -. s .<_ W -> ( ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( s = R -> z = N ) ) ) )
70 69 pm5.74d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ s e. A ) -> ( ( -. s .<_ W -> ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) ) <-> ( -. s .<_ W -> ( s = R -> z = N ) ) ) )
71 impexp 
 |-  ( ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( -. s .<_ W -> ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) ) )
72 bi2.04 
 |-  ( ( s = R -> ( -. s .<_ W -> z = N ) ) <-> ( -. s .<_ W -> ( s = R -> z = N ) ) )
73 70 71 72 3bitr4g 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ s e. A ) -> ( ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( s = R -> ( -. s .<_ W -> z = N ) ) ) )
74 73 ralbidva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> A. s e. A ( s = R -> ( -. s .<_ W -> z = N ) ) ) )
75 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> -. R .<_ W )
76 biimt 
 |-  ( -. R .<_ W -> ( z = [_ R / s ]_ N <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
77 75 76 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( z = [_ R / s ]_ N <-> ( -. R .<_ W -> z = [_ R / s ]_ N ) ) )
78 39 74 77 3bitr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> z = [_ R / s ]_ N ) )
79 78 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) /\ z e. B ) -> ( A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> z = [_ R / s ]_ N ) )
80 25 79 riota5 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) = [_ R / s ]_ N )
81 20 80 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ P =/= Q ) -> [_ R / x ]_ O = [_ R / s ]_ N )