Metamath Proof Explorer


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 )