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 ⊢ 𝐵 = ( 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 eqtrid ⊢ ( 𝑠 = 𝑢 → 𝐺 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐸 ∨ ( ( 𝑢 ∨ 𝑡 ) ∧ 𝑊 ) ) ) )
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 ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = ⦋ 𝑅 / 𝑢 ⦌ 𝑉 )