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 ‘ 𝐾 )
	hlatexch4.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlatexch3N	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		hlatexch4.j	⊢ ∨ = ( join ‘ 𝐾 )
2		hlatexch4.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		simp1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
4		simp21	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
5		simp22	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7	6 1 2	hlatlej2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
8	3 4 5 7	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
9		simp23	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
10	6 1 2	hlatlej2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) )
11	3 4 9 10	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) )
12		simp3r	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) )
13	11 12	breqtrrd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
14		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
15	14	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17	16 2	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
18	5 17	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
19	16 2	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
20	9 19	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
21	16 1 2	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
22	3 4 5 21	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
23	16 6 1	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
24	15 18 20 22 23	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( ( 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
25	8 13 24	mpbi2and	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
26		simp3l	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → 𝑄 ≠ 𝑅 )
27	6 1 2	ps-1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑄 ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
28	3 5 9 26 4 5 27	syl132anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑄 ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
29	25 28	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) )
30	29	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑅 ) )