Metamath Proof Explorer


Theorem cvlsupr6

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

Ref Expression
Hypotheses cvlsupr5.a A = Atoms K
cvlsupr5.j ˙ = join K
Assertion cvlsupr6 K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R Q

Proof

Step Hyp Ref Expression
1 cvlsupr5.a A = Atoms K
2 cvlsupr5.j ˙ = join K
3 eqid K = K
4 1 3 2 cvlsupr2 K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R P R Q R K P ˙ Q
5 simp2 R P R Q R K P ˙ Q R Q
6 4 5 syl6bi K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R Q
7 6 3exp K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R Q
8 7 imp4a K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R Q
9 8 3imp K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R Q