Theorem cdleme40v

Description: Part of proof of Lemma E in Crawley p. 113. Change bound variables in [_ S / u ]_ V (but we use [_ R / u ]_ V for convenience since we have its hypotheses available). (Contributed by NM, 18-Mar-2013)

	Ref	Expression
Hypotheses	cdleme40.b	|- B = ( Base ` K )
	cdleme40.l	|- .<_ = ( le ` K )
	cdleme40.j	|- .\/ = ( join ` K )
	cdleme40.m	|- ./\ = ( meet ` K )
	cdleme40.a	|- A = ( Atoms ` K )
	cdleme40.h	|- H = ( LHyp ` K )
	cdleme40.u	|- U = ( ( P .\/ Q ) ./\ W )
	cdleme40.e	|- E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
	cdleme40.g	|- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
	cdleme40.i	|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
	cdleme40.n	|- N = if ( s .<_ ( P .\/ Q ) , I , D )
	cdleme40.d	|- D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
	cdleme40r.y	|- Y = ( ( u .\/ U ) ./\ ( Q .\/ ( ( P .\/ u ) ./\ W ) ) )
	cdleme40r.t	|- T = ( ( v .\/ U ) ./\ ( Q .\/ ( ( P .\/ v ) ./\ W ) ) )
	cdleme40r.x	|- X = ( ( P .\/ Q ) ./\ ( T .\/ ( ( u .\/ v ) ./\ W ) ) )
	cdleme40r.o	|- O = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) )
	cdleme40r.v	|- V = if ( u .<_ ( P .\/ Q ) , O , Y )
Assertion	cdleme40v	|- ( R e. A -> [_ R / s ]_ N = [_ R / u ]_ V )

Proof

Step	Hyp	Ref	Expression
1		cdleme40.b	|- B = ( Base ` K )
2		cdleme40.l	|- .<_ = ( le ` K )
3		cdleme40.j	|- .\/ = ( join ` K )
4		cdleme40.m	|- ./\ = ( meet ` K )
5		cdleme40.a	|- A = ( Atoms ` K )
6		cdleme40.h	|- H = ( LHyp ` K )
7		cdleme40.u	|- U = ( ( P .\/ Q ) ./\ W )
8		cdleme40.e	|- E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
9		cdleme40.g	|- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
10		cdleme40.i	|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
11		cdleme40.n	|- N = if ( s .<_ ( P .\/ Q ) , I , D )
12		cdleme40.d	|- D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
13		cdleme40r.y	|- Y = ( ( u .\/ U ) ./\ ( Q .\/ ( ( P .\/ u ) ./\ W ) ) )
14		cdleme40r.t	|- T = ( ( v .\/ U ) ./\ ( Q .\/ ( ( P .\/ v ) ./\ W ) ) )
15		cdleme40r.x	|- X = ( ( P .\/ Q ) ./\ ( T .\/ ( ( u .\/ v ) ./\ W ) ) )
16		cdleme40r.o	|- O = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) )
17		cdleme40r.v	|- V = if ( u .<_ ( P .\/ Q ) , O , Y )
18		breq1	|- ( s = u -> ( s .<_ ( P .\/ Q ) <-> u .<_ ( P .\/ Q ) ) )
19		oveq1	|- ( s = u -> ( s .\/ t ) = ( u .\/ t ) )
20	19	oveq1d	|- ( s = u -> ( ( s .\/ t ) ./\ W ) = ( ( u .\/ t ) ./\ W ) )
21	20	oveq2d	|- ( s = u -> ( E .\/ ( ( s .\/ t ) ./\ W ) ) = ( E .\/ ( ( u .\/ t ) ./\ W ) ) )
22	21	oveq2d	|- ( s = u -> ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) )
23	9 22	syl5eq	|- ( s = u -> G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) )
24	23	eqeq2d	|- ( s = u -> ( y = G <-> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) )
25	24	imbi2d	|- ( s = u -> ( ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) <-> ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) )
26	25	ralbidv	|- ( s = u -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) <-> A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) )
27	26	riotabidv	|- ( s = u -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) )
28		eqeq1	|- ( y = z -> ( y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) <-> z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) )
29	28	imbi2d	|- ( y = z -> ( ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) )
30	29	ralbidv	|- ( y = z -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) )
31		breq1	|- ( t = v -> ( t .<_ W <-> v .<_ W ) )
32	31	notbid	|- ( t = v -> ( -. t .<_ W <-> -. v .<_ W ) )
33		breq1	|- ( t = v -> ( t .<_ ( P .\/ Q ) <-> v .<_ ( P .\/ Q ) ) )
34	33	notbid	|- ( t = v -> ( -. t .<_ ( P .\/ Q ) <-> -. v .<_ ( P .\/ Q ) ) )
35	32 34	anbi12d	|- ( t = v -> ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) <-> ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) )
36		oveq1	|- ( t = v -> ( t .\/ U ) = ( v .\/ U ) )
37		oveq2	|- ( t = v -> ( P .\/ t ) = ( P .\/ v ) )
38	37	oveq1d	|- ( t = v -> ( ( P .\/ t ) ./\ W ) = ( ( P .\/ v ) ./\ W ) )
39	38	oveq2d	|- ( t = v -> ( Q .\/ ( ( P .\/ t ) ./\ W ) ) = ( Q .\/ ( ( P .\/ v ) ./\ W ) ) )
40	36 39	oveq12d	|- ( t = v -> ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) ) = ( ( v .\/ U ) ./\ ( Q .\/ ( ( P .\/ v ) ./\ W ) ) ) )
41	40 8 14	3eqtr4g	|- ( t = v -> E = T )
42		oveq2	|- ( t = v -> ( u .\/ t ) = ( u .\/ v ) )
43	42	oveq1d	|- ( t = v -> ( ( u .\/ t ) ./\ W ) = ( ( u .\/ v ) ./\ W ) )
44	41 43	oveq12d	|- ( t = v -> ( E .\/ ( ( u .\/ t ) ./\ W ) ) = ( T .\/ ( ( u .\/ v ) ./\ W ) ) )
45	44	oveq2d	|- ( t = v -> ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( T .\/ ( ( u .\/ v ) ./\ W ) ) ) )
46	45 15	eqtr4di	|- ( t = v -> ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) = X )
47	46	eqeq2d	|- ( t = v -> ( z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) <-> z = X ) )
48	35 47	imbi12d	|- ( t = v -> ( ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) ) )
49	48	cbvralvw	|- ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) )
50	30 49	bitrdi	|- ( y = z -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) ) )
51	50	cbvriotavw	|- ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) )
52	27 51	eqtrdi	|- ( s = u -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) ) )
53	52 10 16	3eqtr4g	|- ( s = u -> I = O )
54		oveq1	|- ( s = u -> ( s .\/ U ) = ( u .\/ U ) )
55		oveq2	|- ( s = u -> ( P .\/ s ) = ( P .\/ u ) )
56	55	oveq1d	|- ( s = u -> ( ( P .\/ s ) ./\ W ) = ( ( P .\/ u ) ./\ W ) )
57	56	oveq2d	|- ( s = u -> ( Q .\/ ( ( P .\/ s ) ./\ W ) ) = ( Q .\/ ( ( P .\/ u ) ./\ W ) ) )
58	54 57	oveq12d	|- ( s = u -> ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( u .\/ U ) ./\ ( Q .\/ ( ( P .\/ u ) ./\ W ) ) ) )
59	58 12 13	3eqtr4g	|- ( s = u -> D = Y )
60	18 53 59	ifbieq12d	|- ( s = u -> if ( s .<_ ( P .\/ Q ) , I , D ) = if ( u .<_ ( P .\/ Q ) , O , Y ) )
61	60 11 17	3eqtr4g	|- ( s = u -> N = V )
62	61	cbvcsbv	|- [_ R / s ]_ N = [_ R / u ]_ V
63	62	a1i	|- ( R e. A -> [_ R / s ]_ N = [_ R / u ]_ V )