hlatexch3N

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

	Ref	Expression
Hypotheses	hlatexch4.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlatexch4.a	$⊢ A = Atoms (K)$
Assertion	hlatexch3N	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} R$

Proof

Step	Hyp	Ref	Expression
1		hlatexch4.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlatexch4.a	$⊢ A = Atoms (K)$
3		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to K \in HL$
4		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to P \in A$
5		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to Q \in A$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7	6 1 2	hlatlej2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \leq_{K} (P \underset{˙}{\lor} Q)$
8	3 4 5 7	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to Q \leq_{K} (P \underset{˙}{\lor} Q)$
9		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to R \in A$
10	6 1 2	hlatlej2	$⊢ (K \in HL \land P \in A \land R \in A) \to R \leq_{K} (P \underset{˙}{\lor} R)$
11	3 4 9 10	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to R \leq_{K} (P \underset{˙}{\lor} R)$
12		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R$
13	11 12	breqtrrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to R \leq_{K} (P \underset{˙}{\lor} Q)$
14		hllat	$⊢ K \in HL \to K \in Lat$
15	14	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to K \in Lat$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
18	5 17	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to Q \in {Base}_{K}$
19	16 2	atbase	$⊢ R \in A \to R \in {Base}_{K}$
20	9 19	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to R \in {Base}_{K}$
21	16 1 2	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
22	3 4 5 21	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
23	16 6 1	latjle12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((Q \leq_{K} (P \underset{˙}{\lor} Q) \land R \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow (Q \underset{˙}{\lor} R) \leq_{K} (P \underset{˙}{\lor} Q))$
24	15 18 20 22 23	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to ((Q \leq_{K} (P \underset{˙}{\lor} Q) \land R \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow (Q \underset{˙}{\lor} R) \leq_{K} (P \underset{˙}{\lor} Q))$
25	8 13 24	mpbi2and	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \leq_{K} (P \underset{˙}{\lor} Q)$
26		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to Q \neq R$
27	6 1 2	ps-1	$⊢ (K \in HL \land (Q \in A \land R \in A \land Q \neq R) \land (P \in A \land Q \in A)) \to ((Q \underset{˙}{\lor} R) \leq_{K} (P \underset{˙}{\lor} Q) \leftrightarrow Q \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
28	3 5 9 26 4 5 27	syl132anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \leq_{K} (P \underset{˙}{\lor} Q) \leftrightarrow Q \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
29	25 28	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} R = P \underset{˙}{\lor} Q$
30	29	eqcomd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} R$

Metamath Proof Explorer

Theorem hlatexch3N

Proof