Metamath Proof Explorer


Theorem dalaw

Description: Desargues's law, derived from Desargues's theorem dath and with no conditions on the atoms. If triples <. P , Q , R >. and <. S , T , U >. are centrally perspective, i.e., ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) , then they are axially perspective. Theorem 13.3 of Crawley p. 110. (Contributed by NM, 7-Oct-2012)

Ref Expression
Hypotheses dalaw.l = ( le ‘ 𝐾 )
dalaw.j = ( join ‘ 𝐾 )
dalaw.m = ( meet ‘ 𝐾 )
dalaw.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion dalaw ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dalaw.l = ( le ‘ 𝐾 )
2 dalaw.j = ( join ‘ 𝐾 )
3 dalaw.m = ( meet ‘ 𝐾 )
4 dalaw.a 𝐴 = ( Atoms ‘ 𝐾 )
5 eqid ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 )
6 1 2 3 4 5 dalawlem14 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
7 6 3expib ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
8 7 3exp ( 𝐾 ∈ HL → ( ¬ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
9 1 2 3 4 5 dalawlem15 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
10 9 3expib ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
11 10 3exp ( 𝐾 ∈ HL → ( ¬ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
12 simp11 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → 𝐾 ∈ HL )
13 simp2 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) )
14 simp3 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) )
15 simp2ll ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) )
16 15 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) )
17 simp2rl ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) )
18 17 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) )
19 simp2lr ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) )
20 19 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) )
21 simp2rr ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) )
22 21 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) )
23 simp13 ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) )
24 1 2 3 4 5 dalawlem1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ) ∧ ( ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
25 12 13 14 16 18 20 22 23 24 syl323anc ( ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
26 25 3expib ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
27 26 3exp ( 𝐾 ∈ HL → ( ( ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑆 𝑇 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑇 𝑈 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑈 𝑆 ) ) ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
28 8 11 27 ecased ( 𝐾 ∈ HL → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) )
29 28 exp4a ( 𝐾 ∈ HL → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) → ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
30 29 com34 ( 𝐾 ∈ HL → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) → ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
31 30 com24 ( 𝐾 ∈ HL → ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) → ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
32 31 3imp ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )