hlsupr2

Description: A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		hlsupr2.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlsupr2.a	$⊢ A = Atoms (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	3 1 2	hlsupr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to \exists r \in A (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))$
5	4	ex	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \to \exists r \in A (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q)))$
6		simpl1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land r \in A) \to K \in HL$
7		hlcvl	$⊢ K \in HL \to K \in CvLat$
8	6 7	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land r \in A) \to K \in CvLat$
9		simpl2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land r \in A) \to P \in A$
10		simpl3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land r \in A) \to Q \in A$
11		simpr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land r \in A) \to r \in A$
12	2 3 1	cvlsupr3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land r \in A)) \to (P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow (P \neq Q \to (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))))$
13	8 9 10 11 12	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land r \in A) \to (P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow (P \neq Q \to (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))))$
14	13	rexbidva	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\exists r \in A P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow \exists r \in A (P \neq Q \to (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))))$
15		ne0i	$⊢ P \in A \to A \neq \emptyset$
16	15	3ad2ant2	$⊢ (K \in HL \land P \in A \land Q \in A) \to A \neq \emptyset$
17		r19.37zv	$⊢ A \neq \emptyset \to (\exists r \in A (P \neq Q \to (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))) \leftrightarrow (P \neq Q \to \exists r \in A (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))))$
18	16 17	syl	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\exists r \in A (P \neq Q \to (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))) \leftrightarrow (P \neq Q \to \exists r \in A (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))))$
19	14 18	bitrd	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\exists r \in A P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow (P \neq Q \to \exists r \in A (r \neq P \land r \neq Q \land r \leq_{K} (P \underset{˙}{\lor} Q))))$
20	5 19	mpbird	$⊢ (K \in HL \land P \in A \land Q \in A) \to \exists r \in A P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r$

Metamath Proof Explorer

Theorem hlsupr2

Proof