Metamath Proof Explorer

Theorem cdleme46f2g2

Description: Conversion for G to reuse F theorems. TODO FIX COMMENT. TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq ? Find other hlatjcom uses giving Q .\/ P . (Contributed by NM, 1-Apr-2013)

		Ref	Expression
	Hypotheses	cdleme46fg.j	$⊢ \underset{˙}{\lor} = join (K)$
		cdleme46fg.a	$⊢ A = Atoms (K)$
	Assertion	cdleme46f2g2	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \neq P \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$

Proof

Step	Hyp	Ref	Expression
1		cdleme46fg.j	$⊢ \underset{˙}{\lor} = join (K)$
2		cdleme46fg.a	$⊢ A = Atoms (K)$
3		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
4		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
5		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
6	3 4 5	3jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W))$
7		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq Q$
8	7	necomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \neq P$
9		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
10	8 9	jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \neq P \land (S \in A \land \neg S \underset{˙}{\leq} W))$
11		simpl1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to K \in HL$
12		simpl2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to P \in A$
13		simpl3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to Q \in A$
14	1 2	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
15	11 12 13 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
16	15	breq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
17	16	notbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
18	17	biimp3a	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
19	6 10 18	3jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \neq P \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$