Theorem cdlemefrs32fva1 33937

Description: Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.)

Hypotheses

Ref	Expression
cdlemefrs27.b	|- B = ( Base ` K )
cdlemefrs27.l	|- .<_ = ( le ` K )
cdlemefrs27.j	|- .\/ = ( join ` K )
cdlemefrs27.m	|- ./\ = ( meet ` K )
cdlemefrs27.a	|- A = ( Atoms ` K )
cdlemefrs27.h	|- H = ( LHyp ` K )
cdlemefrs27.eq	|- ( s = R -> ( ph <-> ps ) )
cdlemefrs27.nb	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> N e. B )
cdlemefrs27.rnb	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> [_ R / s ]_ N e. B )
cdleme29frs.o	|- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
cdleme29frs.f	|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )

Assertion

Ref	Expression
cdlemefrs32fva1	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( F ` R ) = [_ R / s ]_ N )

Distinct variable groups:   z, s, A   H, s   .\/ , s   K, s   .<_ , s   P, s   Q, s   R, s   W, s   ps, s   z, A   z, B   z, H   z, K   z, .<_   z, N   z, P   z, Q   z, R   z, W   ps, z   B, s   z, .\/   ./\ , s, z   ph, z   x, z, A   x, B   x, .\/   x, .<_   x, ./\   x, N   x, s, R   x, W   x, P   x, Q

Allowed substitution hints:   ph( x, s)   ps( x)   F( x, z, s)   H( x)   K( x)   N( s)   O( x, z, s)

Proof of Theorem cdlemefrs32fva1

Step	Hyp	Ref	Expression
1		simp2rl 1074	. . . 4 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> R e. A )
2		cdlemefrs27.b	. . . . 5 |- B = ( Base ` K )
3		cdlemefrs27.a	. . . . 5 |- A = ( Atoms ` K )
4	2, 3	atbase 32824	. . . 4 |- ( R e. A -> R e. B )
5	1, 4	syl 17	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> R e. B )
6		simp2l 1031	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> P =/= Q )
7		simp2rr 1075	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> -. R .<_ W )
8		cdleme29frs.o	. . . 4 |- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
9		cdleme29frs.f	. . . 4 |- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
10	8, 9	cdleme31fv1s 33928	. . 3 |- ( ( R e. B /\ ( P =/= Q /\ -. R .<_ W ) ) -> ( F ` R ) = [_ R / x ]_ O )
11	5, 6, 7, 10	syl12anc 1262	. 2 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( F ` R ) = [_ R / x ]_ O )
12		cdlemefrs27.l	. . 3 |- .<_ = ( le ` K )
13		cdlemefrs27.j	. . 3 |- .\/ = ( join ` K )
14		cdlemefrs27.m	. . 3 |- ./\ = ( meet ` K )
15		cdlemefrs27.h	. . 3 |- H = ( LHyp ` K )
16		cdlemefrs27.eq	. . 3 |- ( s = R -> ( ph <-> ps ) )
17		cdlemefrs27.nb	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> N e. B )
18		cdlemefrs27.rnb	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> [_ R / s ]_ N e. B )
19	2, 12, 13, 14, 3, 15, 16, 17, 18, 8	cdlemefrs32fva 33936	. 2 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> [_ R / x ]_ O = [_ R / s ]_ N )
20	11, 19	eqtrd 2463	1 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( F ` R ) = [_ R / s ]_ N )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1872   =/= wne 2614   A.wral 2771   [_csb 3395   ifcif 3911   class class class wbr 4423   |-> cmpt 4482   ` cfv 5601   iota_crio 6266  (class class class)co 6305   Basecbs 15120   lecple 15196   joincjn 16188   meetcmee 16189   Atomscatm 32798   HLchlt 32885   LHypclh 33518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-preset 16172  df-poset 16190  df-plt 16203  df-lub 16219  df-glb 16220  df-join 16221  df-meet 16222  df-p0 16284  df-p1 16285  df-lat 16291  df-clat 16353  df-oposet 32711  df-ol 32713  df-oml 32714  df-covers 32801  df-ats 32802  df-atl 32833  df-cvlat 32857  df-hlat 32886  df-lhyp 33522

This theorem is referenced by:  cdlemefr32fva1  33946  cdlemefs32fva1  33959