Theorem cvlsupr3

Description: Two equivalent ways of expressing that R is a superposition of P and Q , which can replace the superposition part of ishlat1 , ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) , with the simpler E. z e. A ( x .\/ z ) = ( y .\/ z ) as shown in ishlat3N . (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	cvlsupr2.a	|- A = ( Atoms ` K )
	cvlsupr2.l	|- .<_ = ( le ` K )
	cvlsupr2.j	|- .\/ = ( join ` K )
Assertion	cvlsupr3	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( P =/= Q -> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvlsupr2.a	|- A = ( Atoms ` K )
2		cvlsupr2.l	|- .<_ = ( le ` K )
3		cvlsupr2.j	|- .\/ = ( join ` K )
4		df-ne	|- ( P =/= Q <-> -. P = Q )
5	4	imbi1i	|- ( ( P =/= Q -> ( P .\/ R ) = ( Q .\/ R ) ) <-> ( -. P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) )
6		oveq1	|- ( P = Q -> ( P .\/ R ) = ( Q .\/ R ) )
7	6	biantrur	|- ( ( -. P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) <-> ( ( P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) /\ ( -. P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) ) )
8		pm4.83	|- ( ( ( P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) /\ ( -. P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) ) <-> ( P .\/ R ) = ( Q .\/ R ) )
9	5 7 8	3bitrri	|- ( ( P .\/ R ) = ( Q .\/ R ) <-> ( P =/= Q -> ( P .\/ R ) = ( Q .\/ R ) ) )
10	1 2 3	cvlsupr2	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= Q ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )
11	10	3expia	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( P =/= Q -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) ) )
12	11	pm5.74d	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P =/= Q -> ( P .\/ R ) = ( Q .\/ R ) ) <-> ( P =/= Q -> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) ) )
13	9 12	syl5bb	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( P =/= Q -> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) ) )