This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3dimlem1

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012)

		Ref	Expression
	Hypotheses	3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
		3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		3dim0.a	$⊢ A = Atoms (K)$
	Assertion	3dimlem1	$⊢ ((Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \land P = Q) \to (P \neq R \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land \neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S))$

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
2		3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		3dim0.a	$⊢ A = Atoms (K)$
4		neeq1	$⊢ P = Q \to (P \neq R \leftrightarrow Q \neq R)$
5		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
6	5	breq2d	$⊢ P = Q \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
7	6	notbid	$⊢ P = Q \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \leftrightarrow \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
8	5	oveq1d	$⊢ P = Q \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} S = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
9	8	breq2d	$⊢ P = Q \to (T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S) \leftrightarrow T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
10	9	notbid	$⊢ P = Q \to (\neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S) \leftrightarrow \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
11	4 7 10	3anbi123d	$⊢ P = Q \to ((P \neq R \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land \neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \leftrightarrow (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)))$
12	11	biimparc	$⊢ ((Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \land P = Q) \to (P \neq R \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land \neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S))$