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

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 eqtrid 
 |-  ( 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 )