Metamath Proof Explorer


Theorem 2llnjN

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnj.l = ( le ‘ 𝐾 )
2llnj.j = ( join ‘ 𝐾 )
2llnj.n 𝑁 = ( LLines ‘ 𝐾 )
2llnj.p 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion 2llnjN ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( 𝑋 𝑌 ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 2llnj.l = ( le ‘ 𝐾 )
2 2llnj.j = ( join ‘ 𝐾 )
3 2llnj.n 𝑁 = ( LLines ‘ 𝐾 )
4 2llnj.p 𝑃 = ( LPlanes ‘ 𝐾 )
5 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 5 2 6 3 islln2 ( 𝐾 ∈ HL → ( 𝑋𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ) )
8 simpr ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) )
9 7 8 syl6bi ( 𝐾 ∈ HL → ( 𝑋𝑁 → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) )
10 5 2 6 3 islln2 ( 𝐾 ∈ HL → ( 𝑌𝑁 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) )
11 simpr ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) )
12 10 11 syl6bi ( 𝐾 ∈ HL → ( 𝑌𝑁 → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) )
13 9 12 anim12d ( 𝐾 ∈ HL → ( ( 𝑋𝑁𝑌𝑁 ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) )
14 13 imp ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) )
15 14 3adantr3 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) )
16 15 3adant3 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) )
17 simp2rr ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑋 = ( 𝑞 𝑟 ) )
18 simp3rr ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑌 = ( 𝑠 𝑡 ) )
19 17 18 oveq12d ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( 𝑋 𝑌 ) = ( ( 𝑞 𝑟 ) ( 𝑠 𝑡 ) ) )
20 simp13 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) )
21 breq1 ( 𝑋 = ( 𝑞 𝑟 ) → ( 𝑋 𝑊 ↔ ( 𝑞 𝑟 ) 𝑊 ) )
22 neeq1 ( 𝑋 = ( 𝑞 𝑟 ) → ( 𝑋𝑌 ↔ ( 𝑞 𝑟 ) ≠ 𝑌 ) )
23 21 22 3anbi13d ( 𝑋 = ( 𝑞 𝑟 ) → ( ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ↔ ( ( 𝑞 𝑟 ) 𝑊𝑌 𝑊 ∧ ( 𝑞 𝑟 ) ≠ 𝑌 ) ) )
24 breq1 ( 𝑌 = ( 𝑠 𝑡 ) → ( 𝑌 𝑊 ↔ ( 𝑠 𝑡 ) 𝑊 ) )
25 neeq2 ( 𝑌 = ( 𝑠 𝑡 ) → ( ( 𝑞 𝑟 ) ≠ 𝑌 ↔ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) )
26 24 25 3anbi23d ( 𝑌 = ( 𝑠 𝑡 ) → ( ( ( 𝑞 𝑟 ) 𝑊𝑌 𝑊 ∧ ( 𝑞 𝑟 ) ≠ 𝑌 ) ↔ ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) ) )
27 23 26 sylan9bb ( ( 𝑋 = ( 𝑞 𝑟 ) ∧ 𝑌 = ( 𝑠 𝑡 ) ) → ( ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ↔ ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) ) )
28 17 18 27 syl2anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ↔ ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) ) )
29 20 28 mpbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) )
30 simp11 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝐾 ∈ HL )
31 simp123 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑊𝑃 )
32 simp2ll ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
33 simp2lr ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
34 simp2rl ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑞𝑟 )
35 simp3ll ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
36 simp3lr ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
37 simp3rl ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → 𝑠𝑡 )
38 1 2 6 3 4 2llnjaN ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠𝑡 ) ) ∧ ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) ) → ( ( 𝑞 𝑟 ) ( 𝑠 𝑡 ) ) = 𝑊 )
39 38 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠𝑡 ) ) → ( ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) → ( ( 𝑞 𝑟 ) ( 𝑠 𝑡 ) ) = 𝑊 ) )
40 30 31 32 33 34 35 36 37 39 syl233anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( ( ( 𝑞 𝑟 ) 𝑊 ∧ ( 𝑠 𝑡 ) 𝑊 ∧ ( 𝑞 𝑟 ) ≠ ( 𝑠 𝑡 ) ) → ( ( 𝑞 𝑟 ) ( 𝑠 𝑡 ) ) = 𝑊 ) )
41 29 40 mpd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( ( 𝑞 𝑟 ) ( 𝑠 𝑡 ) ) = 𝑊 )
42 19 41 eqtrd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) ) → ( 𝑋 𝑌 ) = 𝑊 )
43 42 3exp ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) → ( 𝑋 𝑌 ) = 𝑊 ) ) )
44 43 3impib ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) → ( 𝑋 𝑌 ) = 𝑊 ) )
45 44 expd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) → ( 𝑋 𝑌 ) = 𝑊 ) ) )
46 45 rexlimdvv ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) → ( 𝑋 𝑌 ) = 𝑊 ) )
47 46 3exp ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) → ( 𝑋 𝑌 ) = 𝑊 ) ) ) )
48 47 rexlimdvv ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) → ( 𝑋 𝑌 ) = 𝑊 ) ) )
49 48 impd ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞𝑟𝑋 = ( 𝑞 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡𝑌 = ( 𝑠 𝑡 ) ) ) → ( 𝑋 𝑌 ) = 𝑊 ) )
50 16 49 mpd ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑁𝑌𝑁𝑊𝑃 ) ∧ ( 𝑋 𝑊𝑌 𝑊𝑋𝑌 ) ) → ( 𝑋 𝑌 ) = 𝑊 )