Metamath Proof Explorer

Theorem 4atex2-0aOLDN

Description: Same as 4atex2 except that S is zero. (Contributed by NM, 27-May-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 4that.l ⊢ ≤ = ( le ‘ 𝐾 )
4that.j ⊢ ∨ = ( join ‘ 𝐾 )
4that.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4that.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion 4atex2-0aOLDN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 4that.l ⊢ ≤ = ( le ‘ 𝐾 )
2 4that.j ⊢ ∨ = ( join ‘ 𝐾 )
3 4that.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 4that.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 simp32l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝑇 ∈ 𝐴 )
6 simp32r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ¬ 𝑇 ≤ 𝑊 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ HL )
8 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
9 7 8 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ OL )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 3 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
12 5 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
13 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
14 10 2 13 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑇 ) = 𝑇 )
15 9 12 14 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑇 ) = 𝑇 )
16 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝑆 = ( 0. ‘ 𝐾 ) )
17 16 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑇 ) )
18 2 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑇 ) = 𝑇 )
19 7 5 18 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( 𝑇 ∨ 𝑇 ) = 𝑇 )
20 15 17 19 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑇 ) )
21 breq1 ⊢ ( 𝑧 = 𝑇 → ( 𝑧 ≤ 𝑊 ↔ 𝑇 ≤ 𝑊 ) )
22 21 notbid ⊢ ( 𝑧 = 𝑇 → ( ¬ 𝑧 ≤ 𝑊 ↔ ¬ 𝑇 ≤ 𝑊 ) )
23 oveq2 ⊢ ( 𝑧 = 𝑇 → ( 𝑆 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑇 ) )
24 oveq2 ⊢ ( 𝑧 = 𝑇 → ( 𝑇 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑇 ) )
25 23 24 eqeq12d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑇 ) ) )
26 22 25 anbi12d ⊢ ( 𝑧 = 𝑇 → ( ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) ↔ ( ¬ 𝑇 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑇 ) ) ) )
27 26 rspcev ⊢ ( ( 𝑇 ∈ 𝐴 ∧ ( ¬ 𝑇 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑇 ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )
28 5 6 20 27 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )