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

Metamath Proof Explorer

Theorem elpaddatriN

Description: Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	paddfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		paddfval.j	$⊢ \underset{˙}{\lor} = join (K)$
		paddfval.a	$⊢ A = Atoms (K)$
		paddfval.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	Assertion	elpaddatriN	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to S \in (X \underset{˙}{+} \{Q\})$

Proof

Step	Hyp	Ref	Expression
1		paddfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddfval.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddfval.a	$⊢ A = Atoms (K)$
4		paddfval.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		simpl1	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to K \in Lat$
6		simpl2	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to X \subseteq A$
7		simpl3	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to Q \in A$
8	7	snssd	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to \{Q\} \subseteq A$
9		simpr1	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to R \in X$
10		snidg	$⊢ Q \in A \to Q \in \{Q\}$
11	7 10	syl	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to Q \in \{Q\}$
12		simpr2	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to S \in A$
13		simpr3	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to S \underset{˙}{\leq} (R \underset{˙}{\lor} Q)$
14	1 2 3 4	elpaddri	$⊢ ((K \in Lat \land X \subseteq A \land \{Q\} \subseteq A) \land (R \in X \land Q \in \{Q\}) \land (S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to S \in (X \underset{˙}{+} \{Q\})$
15	5 6 8 9 11 12 13 14	syl322anc	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (R \in X \land S \in A \land S \underset{˙}{\leq} (R \underset{˙}{\lor} Q))) \to S \in (X \underset{˙}{+} \{Q\})$