Metamath Proof Explorer

Theorem hlatexch3N

Description: Rearrange join of atoms in an equality. (Contributed by NM, 29-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hlatexch4.j 
|- .\/ = ( join ` K )
hlatexch4.a 
|- A = ( Atoms ` K )
Assertion hlatexch3N 
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( P .\/ Q ) = ( Q .\/ R ) )

Proof

Step Hyp Ref Expression
1 hlatexch4.j 
 |-  .\/ = ( join ` K )
2 hlatexch4.a 
 |-  A = ( Atoms ` K )
3 simp1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> K e. HL )
4 simp21 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> P e. A )
5 simp22 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> Q e. A )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 6 1 2 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q ( le ` K ) ( P .\/ Q ) )
8 3 4 5 7 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> Q ( le ` K ) ( P .\/ Q ) )
9 simp23 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> R e. A )
10 6 1 2 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> R ( le ` K ) ( P .\/ R ) )
11 3 4 9 10 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> R ( le ` K ) ( P .\/ R ) )
12 simp3r 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( P .\/ Q ) = ( P .\/ R ) )
13 11 12 breqtrrd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> R ( le ` K ) ( P .\/ Q ) )
14 hllat 
 |-  ( K e. HL -> K e. Lat )
15 14 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> K e. Lat )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 16 2 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
18 5 17 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> Q e. ( Base ` K ) )
19 16 2 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
20 9 19 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> R e. ( Base ` K ) )
21 16 1 2 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
22 3 4 5 21 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
23 16 6 1 latjle12 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ R e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( Q ( le ` K ) ( P .\/ Q ) /\ R ( le ` K ) ( P .\/ Q ) ) <-> ( Q .\/ R ) ( le ` K ) ( P .\/ Q ) ) )
24 15 18 20 22 23 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( ( Q ( le ` K ) ( P .\/ Q ) /\ R ( le ` K ) ( P .\/ Q ) ) <-> ( Q .\/ R ) ( le ` K ) ( P .\/ Q ) ) )
25 8 13 24 mpbi2and 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( Q .\/ R ) ( le ` K ) ( P .\/ Q ) )
26 simp3l 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> Q =/= R )
27 6 1 2 ps-1 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ Q =/= R ) /\ ( P e. A /\ Q e. A ) ) -> ( ( Q .\/ R ) ( le ` K ) ( P .\/ Q ) <-> ( Q .\/ R ) = ( P .\/ Q ) ) )
28 3 5 9 26 4 5 27 syl132anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( ( Q .\/ R ) ( le ` K ) ( P .\/ Q ) <-> ( Q .\/ R ) = ( P .\/ Q ) ) )
29 25 28 mpbid 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( Q .\/ R ) = ( P .\/ Q ) )
30 29 eqcomd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ ( P .\/ Q ) = ( P .\/ R ) ) ) -> ( P .\/ Q ) = ( Q .\/ R ) )