Metamath Proof Explorer


Theorem cvlsupr5

Description: Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ) . (Contributed by NM, 9-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 cvlsupr5.a 𝐴 = ( Atoms ‘ 𝐾 )
2 cvlsupr5.j = ( join ‘ 𝐾 )
3 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 1 3 2 cvlsupr2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ 𝑃𝑄 ) → ( ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ↔ ( 𝑅𝑃𝑅𝑄𝑅 ( le ‘ 𝐾 ) ( 𝑃 𝑄 ) ) ) )
5 simp1 ( ( 𝑅𝑃𝑅𝑄𝑅 ( le ‘ 𝐾 ) ( 𝑃 𝑄 ) ) → 𝑅𝑃 )
6 4 5 syl6bi ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ 𝑃𝑄 ) → ( ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) → 𝑅𝑃 ) )
7 6 3exp ( 𝐾 ∈ CvLat → ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) → ( 𝑃𝑄 → ( ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) → 𝑅𝑃 ) ) ) )
8 7 imp4a ( 𝐾 ∈ CvLat → ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) → ( ( 𝑃𝑄 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) → 𝑅𝑃 ) ) )
9 8 3imp ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ) → 𝑅𝑃 )