Metamath Proof Explorer


Theorem 4atex3

Description: More general version of 4atex for a line S .\/ T not necessarily connected to P .\/ Q . (Contributed by NM, 29-May-2013)

Ref Expression
Hypotheses 4that.l = ( le ‘ 𝐾 )
4that.j = ( join ‘ 𝐾 )
4that.a 𝐴 = ( Atoms ‘ 𝐾 )
4that.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion 4atex3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑧𝑆𝑧𝑇𝑧 ( 𝑆 𝑇 ) ) ) )

Proof

Step Hyp Ref Expression
1 4that.l = ( le ‘ 𝐾 )
2 4that.j = ( join ‘ 𝐾 )
3 4that.a 𝐴 = ( Atoms ‘ 𝐾 )
4 4that.h 𝐻 = ( LHyp ‘ 𝐾 )
5 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) )
7 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑃𝑄 )
8 simp32l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑇𝐴 )
9 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) )
10 1 2 3 4 4atex2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑇𝐴 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑆 𝑧 ) = ( 𝑇 𝑧 ) ) )
11 5 6 7 8 9 10 syl113anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑆 𝑧 ) = ( 𝑇 𝑧 ) ) )
12 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝐾 ∈ HL )
13 hlcvl ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
14 12 13 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝐾 ∈ CvLat )
15 14 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → 𝐾 ∈ CvLat )
16 simp23l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑆𝐴 )
17 16 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → 𝑆𝐴 )
18 8 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → 𝑇𝐴 )
19 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → 𝑧𝐴 )
20 simp32r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑆𝑇 )
21 20 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → 𝑆𝑇 )
22 3 1 2 cvlsupr2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑆𝐴𝑇𝐴𝑧𝐴 ) ∧ 𝑆𝑇 ) → ( ( 𝑆 𝑧 ) = ( 𝑇 𝑧 ) ↔ ( 𝑧𝑆𝑧𝑇𝑧 ( 𝑆 𝑇 ) ) ) )
23 15 17 18 19 21 22 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → ( ( 𝑆 𝑧 ) = ( 𝑇 𝑧 ) ↔ ( 𝑧𝑆𝑧𝑇𝑧 ( 𝑆 𝑇 ) ) ) )
24 23 anbi2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑧𝐴 ) → ( ( ¬ 𝑧 𝑊 ∧ ( 𝑆 𝑧 ) = ( 𝑇 𝑧 ) ) ↔ ( ¬ 𝑧 𝑊 ∧ ( 𝑧𝑆𝑧𝑇𝑧 ( 𝑆 𝑇 ) ) ) ) )
25 24 rexbidva ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ( ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑆 𝑧 ) = ( 𝑇 𝑧 ) ) ↔ ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑧𝑆𝑧𝑇𝑧 ( 𝑆 𝑇 ) ) ) ) )
26 11 25 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑇𝐴𝑆𝑇 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑧𝑆𝑧𝑇𝑧 ( 𝑆 𝑇 ) ) ) )