hlsupr

Description: A Hilbert lattice has the superposition property. Theorem 13.2 in Crawley p. 107. (Contributed by NM, 30-Jan-2012)

	Ref	Expression
Hypotheses	hlsupr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	hlsupr.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlsupr.a	$⊢ A = Atoms (K)$
Assertion	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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Step	Hyp	Ref	Expression
1		hlsupr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		hlsupr.j	$⊢ \underset{˙}{\lor} = join (K)$
3		hlsupr.a	$⊢ A = Atoms (K)$
4		eqid	$⊢ {Base}_{K} = {Base}_{K}$
5	4 1 2 3	hlsuprexch	$⊢ (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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land \forall r \in {Base}_{K} ((\neg P \underset{˙}{\leq} r \land P \underset{˙}{\leq} (r \underset{˙}{\lor} Q)) \to Q \underset{˙}{\leq} (r \underset{˙}{\lor} P)))$
6	5	simpld	$⊢ (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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
7	6	imp	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer