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. ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑧 ) = ( 𝑇 ∨ 𝑧 ) ) )