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

Metamath Proof Explorer

Theorem 4atex2-0cOLDN

Description: Same as 4atex2 except that S and T are zero. TODO: do we need this one or 4atex2-0aOLDN or 4atex2-0bOLDN ? (Contributed by NM, 27-May-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	4that.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		4that.j	$⊢ \underset{˙}{\lor} = join (K)$
		4that.a	$⊢ A = Atoms (K)$
		4that.h	$⊢ H = LHyp (K)$
	Assertion	4atex2-0cOLDN	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land S \underset{˙}{\lor} z = T \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		4that.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4that.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4that.a	$⊢ A = Atoms (K)$
4		4that.h	$⊢ H = LHyp (K)$
5		simp21l	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \in A$
6		simp21r	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \neg P \underset{˙}{\leq} W$
7		simp23	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to S = 0. (K)$
8	7	oveq1d	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to S \underset{˙}{\lor} P = 0. (K) \underset{˙}{\lor} P$
9		simp32	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to T = 0. (K)$
10	9	oveq1d	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to T \underset{˙}{\lor} P = 0. (K) \underset{˙}{\lor} P$
11	8 10	eqtr4d	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to S \underset{˙}{\lor} P = T \underset{˙}{\lor} P$
12		breq1	$⊢ z = P \to (z \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\leq} W)$
13	12	notbid	$⊢ z = P \to (\neg z \underset{˙}{\leq} W \leftrightarrow \neg P \underset{˙}{\leq} W)$
14		oveq2	$⊢ z = P \to S \underset{˙}{\lor} z = S \underset{˙}{\lor} P$
15		oveq2	$⊢ z = P \to T \underset{˙}{\lor} z = T \underset{˙}{\lor} P$
16	14 15	eqeq12d	$⊢ z = P \to (S \underset{˙}{\lor} z = T \underset{˙}{\lor} z \leftrightarrow S \underset{˙}{\lor} P = T \underset{˙}{\lor} P)$
17	13 16	anbi12d	$⊢ z = P \to ((\neg z \underset{˙}{\leq} W \land S \underset{˙}{\lor} z = T \underset{˙}{\lor} z) \leftrightarrow (\neg P \underset{˙}{\leq} W \land S \underset{˙}{\lor} P = T \underset{˙}{\lor} P))$
18	17	rspcev	$⊢ (P \in A \land (\neg P \underset{˙}{\leq} W \land S \underset{˙}{\lor} P = T \underset{˙}{\lor} P)) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land S \underset{˙}{\lor} z = T \underset{˙}{\lor} z)$
19	5 6 11 18	syl12anc	$⊢ ((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 S = 0. (K)) \land (P \neq Q \land T = 0. (K) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land S \underset{˙}{\lor} z = T \underset{˙}{\lor} z)$