Metamath Proof Explorer


Theorem 4atlem4a

Description: Lemma for 4at . Frequently used associative law. (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l = ( le ‘ 𝐾 )
4at.j = ( join ‘ 𝐾 )
4at.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 4atlem4a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 4at.l = ( le ‘ 𝐾 )
2 4at.j = ( join ‘ 𝐾 )
3 4at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐾 ∈ HL )
5 4 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐾 ∈ Lat )
6 simpl2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑃𝐴 )
7 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
9 6 8 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10 simpl3 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑄𝐴 )
11 7 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13 simprl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑅𝐴 )
14 simprr ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑆𝐴 )
15 7 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
16 4 13 14 15 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17 7 2 latjass ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( 𝑃 ( 𝑄 ( 𝑅 𝑆 ) ) ) )
18 5 9 12 16 17 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( 𝑃 ( 𝑄 ( 𝑅 𝑆 ) ) ) )
19 2 3 hlatjass ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑄 𝑅 ) 𝑆 ) = ( 𝑄 ( 𝑅 𝑆 ) ) )
20 4 10 13 14 19 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑄 𝑅 ) 𝑆 ) = ( 𝑄 ( 𝑅 𝑆 ) ) )
21 20 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) = ( 𝑃 ( 𝑄 ( 𝑅 𝑆 ) ) ) )
22 18 21 eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) )