elpaddat

Description: Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012)

	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	elpaddat	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (S \in (X \underset{˙}{+} \{Q\}) \leftrightarrow (S \in A \land \exists p \in X S \underset{˙}{\leq} (p \underset{˙}{\lor} 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 X \neq \emptyset) \to K \in Lat$
6		simpl2	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to X \subseteq A$
7		simpl3	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to Q \in A$
8	7	snssd	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to \{Q\} \subseteq A$
9		simpr	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to X \neq \emptyset$
10		snnzg	$⊢ Q \in A \to \{Q\} \neq \emptyset$
11	7 10	syl	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to \{Q\} \neq \emptyset$
12	1 2 3 4	elpaddn0	$⊢ ((K \in Lat \land X \subseteq A \land \{Q\} \subseteq A) \land (X \neq \emptyset \land \{Q\} \neq \emptyset)) \to (S \in (X \underset{˙}{+} \{Q\}) \leftrightarrow (S \in A \land \exists p \in X \exists r \in \{Q\} S \underset{˙}{\leq} (p \underset{˙}{\lor} r)))$
13	5 6 8 9 11 12	syl32anc	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (S \in (X \underset{˙}{+} \{Q\}) \leftrightarrow (S \in A \land \exists p \in X \exists r \in \{Q\} S \underset{˙}{\leq} (p \underset{˙}{\lor} r)))$
14		oveq2	$⊢ r = Q \to p \underset{˙}{\lor} r = p \underset{˙}{\lor} Q$
15	14	breq2d	$⊢ r = Q \to (S \underset{˙}{\leq} (p \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (p \underset{˙}{\lor} Q))$
16	15	rexsng	$⊢ Q \in A \to (\exists r \in \{Q\} S \underset{˙}{\leq} (p \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (p \underset{˙}{\lor} Q))$
17	7 16	syl	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (\exists r \in \{Q\} S \underset{˙}{\leq} (p \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (p \underset{˙}{\lor} Q))$
18	17	rexbidv	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (\exists p \in X \exists r \in \{Q\} S \underset{˙}{\leq} (p \underset{˙}{\lor} r) \leftrightarrow \exists p \in X S \underset{˙}{\leq} (p \underset{˙}{\lor} Q))$
19	18	anbi2d	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to ((S \in A \land \exists p \in X \exists r \in \{Q\} S \underset{˙}{\leq} (p \underset{˙}{\lor} r)) \leftrightarrow (S \in A \land \exists p \in X S \underset{˙}{\leq} (p \underset{˙}{\lor} Q)))$
20	13 19	bitrd	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (S \in (X \underset{˙}{+} \{Q\}) \leftrightarrow (S \in A \land \exists p \in X S \underset{˙}{\leq} (p \underset{˙}{\lor} Q)))$

Metamath Proof Explorer

Theorem elpaddat

Proof