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

Metamath Proof Explorer

Theorem cdlemefs29pre00N

Description: FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat . (Contributed by NM, 27-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemefs29.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemefs29.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemefs29.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemefs29.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemefs29.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemefs29.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemefs29pre00N ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemefs29.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemefs29.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemefs29.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemefs29.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlemefs29.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemefs29.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 breq1 ⊢ ( 𝑠 = 𝑅 → ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
8 1 2 3 4 5 6 7 cdlemefrs29pre00 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) )