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

Metamath Proof Explorer

Theorem cdlemc2

Description: Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses cdlemc2.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemc2.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemc2.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemc2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemc2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemc2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemc2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑄 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemc2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemc2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemc2.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdlemc2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemc2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemc2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
8 simp3ll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑃 ∈ 𝐴 )
9 simp3rl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑄 ∈ 𝐴 )
10 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
12 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
15 9 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
16 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
17 13 1 2 3 4 5 cdlemc1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑄 ) )
18 12 15 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑄 ) )
19 11 18 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
20 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐹 ∈ 𝑇 )
21 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
22 13 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 8 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
24 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
25 21 23 15 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
26 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑊 ∈ 𝐻 )
27 13 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28 26 27 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
29 13 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
30 21 25 28 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
31 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
32 21 23 30 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
33 13 1 5 6 ltrnle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ↔ ( 𝐹 ‘ 𝑄 ) ≤ ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) ) )
34 12 20 15 32 33 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ↔ ( 𝐹 ‘ 𝑄 ) ≤ ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) ) )
35 19 34 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑄 ) ≤ ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
36 13 2 5 6 ltrnj ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
37 12 20 23 30 36 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
38 13 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
39 21 25 28 38 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
40 13 1 5 6 ltrnval1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
41 12 20 30 39 40 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
42 41 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
43 37 42 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
44 35 43 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑄 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )