linepmap

Description: A line described with a projective map. (Contributed by NM, 3-Feb-2012)

	Ref	Expression
Hypotheses	isline2.j	$⊢ \underset{˙}{\lor} = join (K)$
	isline2.a	$⊢ A = Atoms (K)$
	isline2.n	$⊢ N = Lines (K)$
	isline2.m	$⊢ M = pmap (K)$
Assertion	linepmap	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to M (P \underset{˙}{\lor} Q) \in N$

Proof

Step	Hyp	Ref	Expression
1		isline2.j	$⊢ \underset{˙}{\lor} = join (K)$
2		isline2.a	$⊢ A = Atoms (K)$
3		isline2.n	$⊢ N = Lines (K)$
4		isline2.m	$⊢ M = pmap (K)$
5		simpl1	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to K \in Lat$
6		simpl2	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to P \in A$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
9	6 8	syl	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to P \in {Base}_{K}$
10		simpl3	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to Q \in A$
11	7 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
12	10 11	syl	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to Q \in {Base}_{K}$
13	7 1	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
14	5 9 12 13	syl3anc	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
15		eqid	$⊢ \leq_{K} = \leq_{K}$
16	7 15 2 4	pmapval	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to M (P \underset{˙}{\lor} Q) = \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\}$
17	5 14 16	syl2anc	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to M (P \underset{˙}{\lor} Q) = \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\}$
18		eqid	$⊢ \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\} = \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\}$
19	15 1 2 3	islinei	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land (P \neq Q \land \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\} = \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\})) \to \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\} \in N$
20	18 19	mpanr2	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to \{r \in A \| r \leq_{K} (P \underset{˙}{\lor} Q)\} \in N$
21	17 20	eqeltrd	$⊢ ((K \in Lat \land P \in A \land Q \in A) \land P \neq Q) \to M (P \underset{˙}{\lor} Q) \in N$

Metamath Proof Explorer

Theorem linepmap

Proof