Metamath Proof Explorer

Theorem paddasslem5

Description: Lemma for paddass . Show s =/= z by contradiction. (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion paddasslem5 ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ) → 𝑠 ≠ 𝑧 )

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 breq1 ⊢ ( 𝑠 = 𝑧 → ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ↔ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) )
5 4 biimpac ⊢ ( ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 = 𝑧 ) → 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝐾 ∈ Lat )
9 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑟 ∈ 𝐴 )
10 6 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
11 9 10 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
12 simp32 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
13 12 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑦 ∈ 𝐴 )
14 6 3 atbase ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
16 simp33 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
17 16 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑧 ∈ 𝐴 )
18 6 3 atbase ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( Base ‘ 𝐾 ) )
19 17 18 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
20 6 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
21 8 15 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( 𝑦 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
22 simp31 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
23 22 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑥 ∈ 𝐴 )
24 6 3 atbase ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( Base ‘ 𝐾 ) )
25 23 24 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
26 6 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
27 8 25 15 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
28 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) )
29 1 2 3 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ ( 𝑥 ∨ 𝑦 ) )
30 7 23 13 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑦 ≤ ( 𝑥 ∨ 𝑦 ) )
31 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) )
32 6 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ↔ ( 𝑦 ∨ 𝑧 ) ≤ ( 𝑥 ∨ 𝑦 ) ) )
33 32 biimpd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( 𝑦 ∨ 𝑧 ) ≤ ( 𝑥 ∨ 𝑦 ) ) )
34 8 15 19 27 33 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( ( 𝑦 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( 𝑦 ∨ 𝑧 ) ≤ ( 𝑥 ∨ 𝑦 ) ) )
35 30 31 34 mp2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( 𝑦 ∨ 𝑧 ) ≤ ( 𝑥 ∨ 𝑦 ) )
36 6 1 8 11 21 27 28 35 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) )
37 36 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → ( 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) )
38 5 37 syl5 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → ( ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 = 𝑧 ) → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) )
39 38 expdimp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( 𝑠 = 𝑧 → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) )
40 39 necon3bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) → 𝑠 ≠ 𝑧 ) )
41 40 exp31 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) → 𝑠 ≠ 𝑧 ) ) ) )
42 41 com23 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) → 𝑠 ≠ 𝑧 ) ) ) )
43 42 com24 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) → 𝑠 ≠ 𝑧 ) ) ) )
44 43 3imp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ) → 𝑠 ≠ 𝑧 )