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

Metamath Proof Explorer

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 bitrid 
 |-  ( ( 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 ) ) ) ) )