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

Metamath Proof Explorer

Theorem 4atex2-0cOLDN

Description: Same as 4atex2 except that S and T are zero. TODO: do we need this one or 4atex2-0aOLDN or 4atex2-0bOLDN ? (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-0cOLDN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 4that.l ⊢ ≤ = ( le ‘ 𝐾 )
2 4that.j ⊢ ∨ = ( join ‘ 𝐾 )
3 4that.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 4that.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝑃 ∈ 𝐴 )
6 simp21r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ¬ 𝑃 ≤ 𝑊 )
7 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝑆 = ( 0. ‘ 𝐾 ) )
8 7 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( 𝑆 ∨ 𝑃 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑃 ) )
9 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → 𝑇 = ( 0. ‘ 𝐾 ) )
10 9 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( 𝑇 ∨ 𝑃 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑃 ) )
11 8 10 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ( 𝑆 ∨ 𝑃 ) = ( 𝑇 ∨ 𝑃 ) )
12 breq1 ⊢ ( 𝑧 = 𝑃 → ( 𝑧 ≤ 𝑊 ↔ 𝑃 ≤ 𝑊 ) )
13 12 notbid ⊢ ( 𝑧 = 𝑃 → ( ¬ 𝑧 ≤ 𝑊 ↔ ¬ 𝑃 ≤ 𝑊 ) )
14 oveq2 ⊢ ( 𝑧 = 𝑃 → ( 𝑆 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑃 ) )
15 oveq2 ⊢ ( 𝑧 = 𝑃 → ( 𝑇 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑃 ) )
16 14 15 eqeq12d ⊢ ( 𝑧 = 𝑃 → ( ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ↔ ( 𝑆 ∨ 𝑃 ) = ( 𝑇 ∨ 𝑃 ) ) )
17 13 16 anbi12d ⊢ ( 𝑧 = 𝑃 → ( ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) ↔ ( ¬ 𝑃 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑃 ) = ( 𝑇 ∨ 𝑃 ) ) ) )
18 17 rspcev ⊢ ( ( 𝑃 ∈ 𝐴 ∧ ( ¬ 𝑃 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑃 ) = ( 𝑇 ∨ 𝑃 ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )
19 5 6 11 18 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 = ( 0. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )