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 HL P A Q A R 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 HL P A Q A R A Q R P ˙ Q = P ˙ R K HL
4 simp21 K HL P A Q A R A Q R P ˙ Q = P ˙ R P A
5 simp22 K HL P A Q A R A Q R P ˙ Q = P ˙ R Q A
6 eqid K = K
7 6 1 2 hlatlej2 K HL P A Q A Q K P ˙ Q
8 3 4 5 7 syl3anc K HL P A Q A R A Q R P ˙ Q = P ˙ R Q K P ˙ Q
9 simp23 K HL P A Q A R A Q R P ˙ Q = P ˙ R R A
10 6 1 2 hlatlej2 K HL P A R A R K P ˙ R
11 3 4 9 10 syl3anc K HL P A Q A R A Q R P ˙ Q = P ˙ R R K P ˙ R
12 simp3r K HL P A Q A R A Q R P ˙ Q = P ˙ R P ˙ Q = P ˙ R
13 11 12 breqtrrd K HL P A Q A R A Q R P ˙ Q = P ˙ R R K P ˙ Q
14 hllat K HL K Lat
15 14 3ad2ant1 K HL P A Q A R A Q R P ˙ Q = P ˙ R K Lat
16 eqid Base K = Base K
17 16 2 atbase Q A Q Base K
18 5 17 syl K HL P A Q A R A Q R P ˙ Q = P ˙ R Q Base K
19 16 2 atbase R A R Base K
20 9 19 syl K HL P A Q A R A Q R P ˙ Q = P ˙ R R Base K
21 16 1 2 hlatjcl K HL P A Q A P ˙ Q Base K
22 3 4 5 21 syl3anc K HL P A Q A R A Q R P ˙ Q = P ˙ R P ˙ Q Base K
23 16 6 1 latjle12 K Lat Q Base K R Base K P ˙ Q Base K Q K P ˙ Q R K P ˙ Q Q ˙ R K P ˙ Q
24 15 18 20 22 23 syl13anc K HL P A Q A R A Q R P ˙ Q = P ˙ R Q K P ˙ Q R K P ˙ Q Q ˙ R K P ˙ Q
25 8 13 24 mpbi2and K HL P A Q A R A Q R P ˙ Q = P ˙ R Q ˙ R K P ˙ Q
26 simp3l K HL P A Q A R A Q R P ˙ Q = P ˙ R Q R
27 6 1 2 ps-1 K HL Q A R A Q R P A Q A Q ˙ R K P ˙ Q Q ˙ R = P ˙ Q
28 3 5 9 26 4 5 27 syl132anc K HL P A Q A R A Q R P ˙ Q = P ˙ R Q ˙ R K P ˙ Q Q ˙ R = P ˙ Q
29 25 28 mpbid K HL P A Q A R A Q R P ˙ Q = P ˙ R Q ˙ R = P ˙ Q
30 29 eqcomd K HL P A Q A R A Q R P ˙ Q = P ˙ R P ˙ Q = Q ˙ R