This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlatj4

Description: Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 for atoms. (Contributed by NM, 9-Aug-2012)

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

Proof

Step Hyp Ref Expression
1 hlatjcom.j ⊢ ∨ = ( join ‘ 𝐾 )
2 hlatjcom.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
4 3 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
5 simp2l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
8 5 7 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9 simp2r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
10 6 2 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
11 9 10 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
13 6 2 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
16 6 2 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
17 15 16 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
18 6 1 latj4 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∨ ( 𝑄 ∨ 𝑆 ) ) )
19 4 8 11 14 17 18 syl122anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∨ ( 𝑄 ∨ 𝑆 ) ) )