Metamath Proof Explorer


Theorem 4at

Description: Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 and 3at . (Contributed by NM, 11-Jul-2012)

Ref Expression
Hypotheses 4at.l = ( le ‘ 𝐾 )
4at.j = ( join ‘ 𝐾 )
4at.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 4at ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 4at.l = ( le ‘ 𝐾 )
2 4at.j = ( join ‘ 𝐾 )
3 4at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 4atlem12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
5 simp11 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → 𝐾 ∈ HL )
6 5 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → 𝐾 ∈ Lat )
7 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → 𝑇𝐴 )
8 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → 𝑈𝐴 )
9 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴 ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
11 5 7 8 10 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
12 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → 𝑉𝐴 )
13 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → 𝑊𝐴 )
14 9 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑉𝐴𝑊𝐴 ) → ( 𝑉 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
15 5 12 13 14 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → ( 𝑉 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
16 9 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑉 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
17 6 11 15 16 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
18 9 1 latref ( ( 𝐾 ∈ Lat ∧ ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
19 6 17 18 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
20 breq1 ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
21 19 20 syl5ibrcom ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
22 21 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
23 4 22 impbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )