hlatexch4

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

Proof

Step	Hyp	Ref	Expression
1		hlatexch4.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlatexch4.a	$⊢ A = Atoms (K)$
3		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to K \in HL$
4		simp2l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to R \in A$
5		simp2r	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to S \in A$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7	6 1 2	hlatlej2	$⊢ (K \in HL \land R \in A \land S \in A) \to S \leq_{K} (R \underset{˙}{\lor} S)$
8	3 4 5 7	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to S \leq_{K} (R \underset{˙}{\lor} S)$
9		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S$
10	8 9	breqtrrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to S \leq_{K} (P \underset{˙}{\lor} Q)$
11		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \in A$
12		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to Q \in A$
13		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to Q \neq S$
14	13	necomd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to S \neq Q$
15	6 1 2	hlatexch2	$⊢ (K \in HL \land (S \in A \land P \in A \land Q \in A) \land S \neq Q) \to (S \leq_{K} (P \underset{˙}{\lor} Q) \to P \leq_{K} (S \underset{˙}{\lor} Q))$
16	3 5 11 12 14 15	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to (S \leq_{K} (P \underset{˙}{\lor} Q) \to P \leq_{K} (S \underset{˙}{\lor} Q))$
17	10 16	mpd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \leq_{K} (S \underset{˙}{\lor} Q)$
18	1 2	hlatjcom	$⊢ (K \in HL \land S \in A \land Q \in A) \to S \underset{˙}{\lor} Q = Q \underset{˙}{\lor} S$
19	3 5 12 18	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to S \underset{˙}{\lor} Q = Q \underset{˙}{\lor} S$
20	17 19	breqtrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \leq_{K} (Q \underset{˙}{\lor} S)$
21	6 1 2	hlatlej2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \leq_{K} (P \underset{˙}{\lor} Q)$
22	3 11 12 21	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to Q \leq_{K} (P \underset{˙}{\lor} Q)$
23	22 9	breqtrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to Q \leq_{K} (R \underset{˙}{\lor} S)$
24	6 1 2	hlatexch2	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Q \neq S) \to (Q \leq_{K} (R \underset{˙}{\lor} S) \to R \leq_{K} (Q \underset{˙}{\lor} S))$
25	3 12 4 5 13 24	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to (Q \leq_{K} (R \underset{˙}{\lor} S) \to R \leq_{K} (Q \underset{˙}{\lor} S))$
26	23 25	mpd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to R \leq_{K} (Q \underset{˙}{\lor} S)$
27	3	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to K \in Lat$
28		eqid	$⊢ {Base}_{K} = {Base}_{K}$
29	28 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
30	11 29	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \in {Base}_{K}$
31	28 2	atbase	$⊢ R \in A \to R \in {Base}_{K}$
32	4 31	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to R \in {Base}_{K}$
33	28 1 2	hlatjcl	$⊢ (K \in HL \land Q \in A \land S \in A) \to Q \underset{˙}{\lor} S \in {Base}_{K}$
34	3 12 5 33	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to Q \underset{˙}{\lor} S \in {Base}_{K}$
35	28 6 1	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land R \in {Base}_{K} \land Q \underset{˙}{\lor} S \in {Base}_{K})) \to ((P \leq_{K} (Q \underset{˙}{\lor} S) \land R \leq_{K} (Q \underset{˙}{\lor} S)) \leftrightarrow (P \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} S))$
36	27 30 32 34 35	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to ((P \leq_{K} (Q \underset{˙}{\lor} S) \land R \leq_{K} (Q \underset{˙}{\lor} S)) \leftrightarrow (P \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} S))$
37	20 26 36	mpbi2and	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to (P \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} S)$
38		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \neq R$
39	6 1 2	ps-1	$⊢ (K \in HL \land (P \in A \land R \in A \land P \neq R) \land (Q \in A \land S \in A)) \to ((P \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} S) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} S)$
40	3 11 4 38 12 5 39	syl132anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} S) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} S)$
41	37 40	mpbid	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq R \land Q \neq S \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} S$

Metamath Proof Explorer

Theorem hlatexch4

Proof