Metamath Proof Explorer


Theorem hlatj32

Description: Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 for atoms. (Contributed by NM, 21-Jul-2012)

Ref Expression
Hypotheses hlatjcom.j = ( join ‘ 𝐾 )
hlatjcom.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlatj32 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑃 𝑅 ) 𝑄 ) )

Proof

Step Hyp Ref Expression
1 hlatjcom.j = ( join ‘ 𝐾 )
2 hlatjcom.a 𝐴 = ( Atoms ‘ 𝐾 )
3 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
4 3 adantr ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝐾 ∈ Lat )
5 simpr1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑃𝐴 )
6 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
8 5 7 syl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9 simpr2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑄𝐴 )
10 6 2 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
11 9 10 syl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12 simpr3 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑅𝐴 )
13 6 2 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 6 1 latj32 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑃 𝑅 ) 𝑄 ) )
16 4 8 11 14 15 syl13anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑃 𝑅 ) 𝑄 ) )