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 𝐵 = ( Base ‘ 𝐾 )
cdleme40.l = ( le ‘ 𝐾 )
cdleme40.j = ( join ‘ 𝐾 )
cdleme40.m = ( meet ‘ 𝐾 )
cdleme40.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme40.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme40.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme40.e 𝐸 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
cdleme40.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdleme40.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) )
cdleme40.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
cdleme40.d 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
cdleme40r.y 𝑌 = ( ( 𝑢 𝑈 ) ( 𝑄 ( ( 𝑃 𝑢 ) 𝑊 ) ) )
cdleme40r.t 𝑇 = ( ( 𝑣 𝑈 ) ( 𝑄 ( ( 𝑃 𝑣 ) 𝑊 ) ) )
cdleme40r.x 𝑋 = ( ( 𝑃 𝑄 ) ( 𝑇 ( ( 𝑢 𝑣 ) 𝑊 ) ) )
cdleme40r.o 𝑂 = ( 𝑧𝐵𝑣𝐴 ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) )
cdleme40r.v 𝑉 = if ( 𝑢 ( 𝑃 𝑄 ) , 𝑂 , 𝑌 )
Assertion cdleme40v ( 𝑅𝐴 𝑅 / 𝑠 𝑁 = 𝑅 / 𝑢 𝑉 )

Proof

Step Hyp Ref Expression
1 cdleme40.b 𝐵 = ( Base ‘ 𝐾 )
2 cdleme40.l = ( le ‘ 𝐾 )
3 cdleme40.j = ( join ‘ 𝐾 )
4 cdleme40.m = ( meet ‘ 𝐾 )
5 cdleme40.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme40.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme40.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdleme40.e 𝐸 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
9 cdleme40.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
10 cdleme40.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) )
11 cdleme40.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
12 cdleme40.d 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
13 cdleme40r.y 𝑌 = ( ( 𝑢 𝑈 ) ( 𝑄 ( ( 𝑃 𝑢 ) 𝑊 ) ) )
14 cdleme40r.t 𝑇 = ( ( 𝑣 𝑈 ) ( 𝑄 ( ( 𝑃 𝑣 ) 𝑊 ) ) )
15 cdleme40r.x 𝑋 = ( ( 𝑃 𝑄 ) ( 𝑇 ( ( 𝑢 𝑣 ) 𝑊 ) ) )
16 cdleme40r.o 𝑂 = ( 𝑧𝐵𝑣𝐴 ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) )
17 cdleme40r.v 𝑉 = if ( 𝑢 ( 𝑃 𝑄 ) , 𝑂 , 𝑌 )
18 breq1 ( 𝑠 = 𝑢 → ( 𝑠 ( 𝑃 𝑄 ) ↔ 𝑢 ( 𝑃 𝑄 ) ) )
19 oveq1 ( 𝑠 = 𝑢 → ( 𝑠 𝑡 ) = ( 𝑢 𝑡 ) )
20 19 oveq1d ( 𝑠 = 𝑢 → ( ( 𝑠 𝑡 ) 𝑊 ) = ( ( 𝑢 𝑡 ) 𝑊 ) )
21 20 oveq2d ( 𝑠 = 𝑢 → ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) = ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) )
22 21 oveq2d ( 𝑠 = 𝑢 → ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) )
23 9 22 syl5eq ( 𝑠 = 𝑢𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) )
24 23 eqeq2d ( 𝑠 = 𝑢 → ( 𝑦 = 𝐺𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) )
25 24 imbi2d ( 𝑠 = 𝑢 → ( ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) ↔ ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ) )
26 25 ralbidv ( 𝑠 = 𝑢 → ( ∀ 𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) ↔ ∀ 𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ) )
27 26 riotabidv ( 𝑠 = 𝑢 → ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) ) = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ) )
28 eqeq1 ( 𝑦 = 𝑧 → ( 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ↔ 𝑧 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) )
29 28 imbi2d ( 𝑦 = 𝑧 → ( ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ↔ ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑧 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ) )
30 29 ralbidv ( 𝑦 = 𝑧 → ( ∀ 𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ↔ ∀ 𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑧 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ) )
31 breq1 ( 𝑡 = 𝑣 → ( 𝑡 𝑊𝑣 𝑊 ) )
32 31 notbid ( 𝑡 = 𝑣 → ( ¬ 𝑡 𝑊 ↔ ¬ 𝑣 𝑊 ) )
33 breq1 ( 𝑡 = 𝑣 → ( 𝑡 ( 𝑃 𝑄 ) ↔ 𝑣 ( 𝑃 𝑄 ) ) )
34 33 notbid ( 𝑡 = 𝑣 → ( ¬ 𝑡 ( 𝑃 𝑄 ) ↔ ¬ 𝑣 ( 𝑃 𝑄 ) ) )
35 32 34 anbi12d ( 𝑡 = 𝑣 → ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ↔ ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) )
36 oveq1 ( 𝑡 = 𝑣 → ( 𝑡 𝑈 ) = ( 𝑣 𝑈 ) )
37 oveq2 ( 𝑡 = 𝑣 → ( 𝑃 𝑡 ) = ( 𝑃 𝑣 ) )
38 37 oveq1d ( 𝑡 = 𝑣 → ( ( 𝑃 𝑡 ) 𝑊 ) = ( ( 𝑃 𝑣 ) 𝑊 ) )
39 38 oveq2d ( 𝑡 = 𝑣 → ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) = ( 𝑄 ( ( 𝑃 𝑣 ) 𝑊 ) ) )
40 36 39 oveq12d ( 𝑡 = 𝑣 → ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) ) = ( ( 𝑣 𝑈 ) ( 𝑄 ( ( 𝑃 𝑣 ) 𝑊 ) ) ) )
41 40 8 14 3eqtr4g ( 𝑡 = 𝑣𝐸 = 𝑇 )
42 oveq2 ( 𝑡 = 𝑣 → ( 𝑢 𝑡 ) = ( 𝑢 𝑣 ) )
43 42 oveq1d ( 𝑡 = 𝑣 → ( ( 𝑢 𝑡 ) 𝑊 ) = ( ( 𝑢 𝑣 ) 𝑊 ) )
44 41 43 oveq12d ( 𝑡 = 𝑣 → ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) = ( 𝑇 ( ( 𝑢 𝑣 ) 𝑊 ) ) )
45 44 oveq2d ( 𝑡 = 𝑣 → ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝑇 ( ( 𝑢 𝑣 ) 𝑊 ) ) ) )
46 45 15 eqtr4di ( 𝑡 = 𝑣 → ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) = 𝑋 )
47 46 eqeq2d ( 𝑡 = 𝑣 → ( 𝑧 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ↔ 𝑧 = 𝑋 ) )
48 35 47 imbi12d ( 𝑡 = 𝑣 → ( ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑧 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ↔ ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) ) )
49 48 cbvralvw ( ∀ 𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑧 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ↔ ∀ 𝑣𝐴 ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) )
50 30 49 bitrdi ( 𝑦 = 𝑧 → ( ∀ 𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ↔ ∀ 𝑣𝐴 ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) ) )
51 50 cbvriotavw ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑢 𝑡 ) 𝑊 ) ) ) ) ) = ( 𝑧𝐵𝑣𝐴 ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) )
52 27 51 eqtrdi ( 𝑠 = 𝑢 → ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) ) = ( 𝑧𝐵𝑣𝐴 ( ( ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) → 𝑧 = 𝑋 ) ) )
53 52 10 16 3eqtr4g ( 𝑠 = 𝑢𝐼 = 𝑂 )
54 oveq1 ( 𝑠 = 𝑢 → ( 𝑠 𝑈 ) = ( 𝑢 𝑈 ) )
55 oveq2 ( 𝑠 = 𝑢 → ( 𝑃 𝑠 ) = ( 𝑃 𝑢 ) )
56 55 oveq1d ( 𝑠 = 𝑢 → ( ( 𝑃 𝑠 ) 𝑊 ) = ( ( 𝑃 𝑢 ) 𝑊 ) )
57 56 oveq2d ( 𝑠 = 𝑢 → ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) = ( 𝑄 ( ( 𝑃 𝑢 ) 𝑊 ) ) )
58 54 57 oveq12d ( 𝑠 = 𝑢 → ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) ) = ( ( 𝑢 𝑈 ) ( 𝑄 ( ( 𝑃 𝑢 ) 𝑊 ) ) ) )
59 58 12 13 3eqtr4g ( 𝑠 = 𝑢𝐷 = 𝑌 )
60 18 53 59 ifbieq12d ( 𝑠 = 𝑢 → if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 ) = if ( 𝑢 ( 𝑃 𝑄 ) , 𝑂 , 𝑌 ) )
61 60 11 17 3eqtr4g ( 𝑠 = 𝑢𝑁 = 𝑉 )
62 61 cbvcsbv 𝑅 / 𝑠 𝑁 = 𝑅 / 𝑢 𝑉
63 62 a1i ( 𝑅𝐴 𝑅 / 𝑠 𝑁 = 𝑅 / 𝑢 𝑉 )