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