atexchcvrN

Description: Atom exchange property. Version of hlatexch2 with covers relation. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atexchcvr.j	$⊢ \underset{˙}{\lor} = join (K)$
	atexchcvr.a	$⊢ A = Atoms (K)$
	atexchcvr.c	$⊢ C = ⋖_{K}$
Assertion	atexchcvrN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P C (Q \underset{˙}{\lor} R) \to Q C (P \underset{˙}{\lor} R))$

Proof

Step	Hyp	Ref	Expression
1		atexchcvr.j	$⊢ \underset{˙}{\lor} = join (K)$
2		atexchcvr.a	$⊢ A = Atoms (K)$
3		atexchcvr.c	$⊢ C = ⋖_{K}$
4		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to K \in HL$
5		simpl21	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to P \in A$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
8	5 7	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to P \in {Base}_{K}$
9	4	hllatd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to K \in Lat$
10		simpl22	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to Q \in A$
11	6 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
12	10 11	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to Q \in {Base}_{K}$
13		simpl23	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to R \in A$
14	6 2	atbase	$⊢ R \in A \to R \in {Base}_{K}$
15	13 14	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to R \in {Base}_{K}$
16	6 1	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
17	9 12 15 16	syl3anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
18	4 8 17	3jca	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to (K \in HL \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20	6 19 3	cvrle	$⊢ ((K \in HL \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land P C (Q \underset{˙}{\lor} R)) \to P \leq_{K} (Q \underset{˙}{\lor} R)$
21	18 20	sylancom	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land P C (Q \underset{˙}{\lor} R)) \to P \leq_{K} (Q \underset{˙}{\lor} R)$
22	21	ex	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P C (Q \underset{˙}{\lor} R) \to P \leq_{K} (Q \underset{˙}{\lor} R))$
23	19 1 2	hlatexch2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \leq_{K} (Q \underset{˙}{\lor} R) \to Q \leq_{K} (P \underset{˙}{\lor} R))$
24		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to K \in HL$
25		simpl22	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to Q \in A$
26		simpl21	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to P \in A$
27		simpl23	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to R \in A$
28		simpl3	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to P \neq R$
29		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to Q \leq_{K} (P \underset{˙}{\lor} R)$
30	19 1 3 2	atcvrj2	$⊢ (K \in HL \land (Q \in A \land P \in A \land R \in A) \land (P \neq R \land Q \leq_{K} (P \underset{˙}{\lor} R))) \to Q C (P \underset{˙}{\lor} R)$
31	24 25 26 27 28 29 30	syl132anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \land Q \leq_{K} (P \underset{˙}{\lor} R)) \to Q C (P \underset{˙}{\lor} R)$
32	31	ex	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (Q \leq_{K} (P \underset{˙}{\lor} R) \to Q C (P \underset{˙}{\lor} R))$
33	22 23 32	3syld	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P C (Q \underset{˙}{\lor} R) \to Q C (P \underset{˙}{\lor} R))$

Metamath Proof Explorer

Theorem atexchcvrN

Proof