pmapjat1

Description: The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012)

	Ref	Expression
Hypotheses	pmapjat.b	$⊢ B = {Base}_{K}$
	pmapjat.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmapjat.a	$⊢ A = Atoms (K)$
	pmapjat.m	$⊢ M = pmap (K)$
	pmapjat.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmapjat1	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (X \underset{˙}{\lor} Q) = M (X) \underset{˙}{+} M (Q)$

Proof

Step	Hyp	Ref	Expression
1		pmapjat.b	$⊢ B = {Base}_{K}$
2		pmapjat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pmapjat.a	$⊢ A = Atoms (K)$
4		pmapjat.m	$⊢ M = pmap (K)$
5		pmapjat.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
6		simp1	$⊢ (K \in HL \land X \in B \land Q \in A) \to K \in HL$
7	1 3	atbase	$⊢ Q \in A \to Q \in B$
8	7	3ad2ant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to Q \in B$
9	1 3 4	pmapssat	$⊢ (K \in HL \land Q \in B) \to M (Q) \subseteq A$
10	6 8 9	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q) \subseteq A$
11	3 5	padd02	$⊢ (K \in HL \land M (Q) \subseteq A) \to \emptyset \underset{˙}{+} M (Q) = M (Q)$
12	6 10 11	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to \emptyset \underset{˙}{+} M (Q) = M (Q)$
13	12	adantr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X = 0. (K)) \to \emptyset \underset{˙}{+} M (Q) = M (Q)$
14		fveq2	$⊢ X = 0. (K) \to M (X) = M (0. (K))$
15		hlatl	$⊢ K \in HL \to K \in AtLat$
16	15	3ad2ant1	$⊢ (K \in HL \land X \in B \land Q \in A) \to K \in AtLat$
17		eqid	$⊢ 0. (K) = 0. (K)$
18	17 4	pmap0	$⊢ K \in AtLat \to M (0. (K)) = \emptyset$
19	16 18	syl	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (0. (K)) = \emptyset$
20	14 19	sylan9eqr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X = 0. (K)) \to M (X) = \emptyset$
21	20	oveq1d	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X = 0. (K)) \to M (X) \underset{˙}{+} M (Q) = \emptyset \underset{˙}{+} M (Q)$
22		oveq1	$⊢ X = 0. (K) \to X \underset{˙}{\lor} Q = 0. (K) \underset{˙}{\lor} Q$
23		hlol	$⊢ K \in HL \to K \in OL$
24	23	3ad2ant1	$⊢ (K \in HL \land X \in B \land Q \in A) \to K \in OL$
25	1 2 17	olj02	$⊢ (K \in OL \land Q \in B) \to 0. (K) \underset{˙}{\lor} Q = Q$
26	24 8 25	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to 0. (K) \underset{˙}{\lor} Q = Q$
27	22 26	sylan9eqr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X = 0. (K)) \to X \underset{˙}{\lor} Q = Q$
28	27	fveq2d	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X = 0. (K)) \to M (X \underset{˙}{\lor} Q) = M (Q)$
29	13 21 28	3eqtr4rd	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X = 0. (K)) \to M (X \underset{˙}{\lor} Q) = M (X) \underset{˙}{+} M (Q)$
30		simpll1	$⊢ (((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \to K \in HL$
31	30	adantr	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to K \in HL$
32		simpll2	$⊢ (((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \to X \in B$
33	32	adantr	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to X \in B$
34		simplr	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to p \in A$
35		simpll3	$⊢ (((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \to Q \in A$
36	35	adantr	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to Q \in A$
37	33 34 36	3jca	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to (X \in B \land p \in A \land Q \in A)$
38		simpllr	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to X \neq 0. (K)$
39		simpr	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to p \leq_{K} (X \underset{˙}{\lor} Q)$
40		eqid	$⊢ \leq_{K} = \leq_{K}$
41	1 40 2 17 3	cvrat42	$⊢ (K \in HL \land (X \in B \land p \in A \land Q \in A)) \to ((X \neq 0. (K) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to \exists q \in A (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q)))$
42	41	imp	$⊢ ((K \in HL \land (X \in B \land p \in A \land Q \in A)) \land (X \neq 0. (K) \land p \leq_{K} (X \underset{˙}{\lor} Q))) \to \exists q \in A (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q))$
43	31 37 38 39 42	syl22anc	$⊢ ((((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to \exists q \in A (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q))$
44	43	ex	$⊢ (((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \to (p \leq_{K} (X \underset{˙}{\lor} Q) \to \exists q \in A (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q)))$
45	1 40 3 4	elpmap	$⊢ (K \in HL \land X \in B) \to (q \in M (X) \leftrightarrow (q \in A \land q \leq_{K} X))$
46	45	3adant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to (q \in M (X) \leftrightarrow (q \in A \land q \leq_{K} X))$
47		df-rex	$⊢ \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r) \leftrightarrow \exists r (r \in M (Q) \land p \leq_{K} (q \underset{˙}{\lor} r))$
48	3 4	elpmapat	$⊢ (K \in HL \land Q \in A) \to (r \in M (Q) \leftrightarrow r = Q)$
49	48	3adant2	$⊢ (K \in HL \land X \in B \land Q \in A) \to (r \in M (Q) \leftrightarrow r = Q)$
50	49	anbi1d	$⊢ (K \in HL \land X \in B \land Q \in A) \to ((r \in M (Q) \land p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow (r = Q \land p \leq_{K} (q \underset{˙}{\lor} r)))$
51	50	exbidv	$⊢ (K \in HL \land X \in B \land Q \in A) \to (\exists r (r \in M (Q) \land p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow \exists r (r = Q \land p \leq_{K} (q \underset{˙}{\lor} r)))$
52	47 51	bitr2id	$⊢ (K \in HL \land X \in B \land Q \in A) \to (\exists r (r = Q \land p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r))$
53		oveq2	$⊢ r = Q \to q \underset{˙}{\lor} r = q \underset{˙}{\lor} Q$
54	53	breq2d	$⊢ r = Q \to (p \leq_{K} (q \underset{˙}{\lor} r) \leftrightarrow p \leq_{K} (q \underset{˙}{\lor} Q))$
55	54	ceqsexgv	$⊢ Q \in A \to (\exists r (r = Q \land p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow p \leq_{K} (q \underset{˙}{\lor} Q))$
56	55	3ad2ant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to (\exists r (r = Q \land p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow p \leq_{K} (q \underset{˙}{\lor} Q))$
57	52 56	bitr3d	$⊢ (K \in HL \land X \in B \land Q \in A) \to (\exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r) \leftrightarrow p \leq_{K} (q \underset{˙}{\lor} Q))$
58	46 57	anbi12d	$⊢ (K \in HL \land X \in B \land Q \in A) \to ((q \in M (X) \land \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow ((q \in A \land q \leq_{K} X) \land p \leq_{K} (q \underset{˙}{\lor} Q)))$
59		anass	$⊢ ((q \in A \land q \leq_{K} X) \land p \leq_{K} (q \underset{˙}{\lor} Q)) \leftrightarrow (q \in A \land (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q)))$
60	58 59	bitrdi	$⊢ (K \in HL \land X \in B \land Q \in A) \to ((q \in M (X) \land \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r)) \leftrightarrow (q \in A \land (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q))))$
61	60	rexbidv2	$⊢ (K \in HL \land X \in B \land Q \in A) \to (\exists q \in M (X) \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r) \leftrightarrow \exists q \in A (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q)))$
62	61	ad2antrr	$⊢ (((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \to (\exists q \in M (X) \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r) \leftrightarrow \exists q \in A (q \leq_{K} X \land p \leq_{K} (q \underset{˙}{\lor} Q)))$
63	44 62	sylibrd	$⊢ (((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \land p \in A) \to (p \leq_{K} (X \underset{˙}{\lor} Q) \to \exists q \in M (X) \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r))$
64	63	imdistanda	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to ((p \in A \land p \leq_{K} (X \underset{˙}{\lor} Q)) \to (p \in A \land \exists q \in M (X) \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r)))$
65		hllat	$⊢ K \in HL \to K \in Lat$
66	65	3ad2ant1	$⊢ (K \in HL \land X \in B \land Q \in A) \to K \in Lat$
67		simp2	$⊢ (K \in HL \land X \in B \land Q \in A) \to X \in B$
68	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Q \in B) \to X \underset{˙}{\lor} Q \in B$
69	66 67 8 68	syl3anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to X \underset{˙}{\lor} Q \in B$
70	1 40 3 4	elpmap	$⊢ (K \in HL \land X \underset{˙}{\lor} Q \in B) \to (p \in M (X \underset{˙}{\lor} Q) \leftrightarrow (p \in A \land p \leq_{K} (X \underset{˙}{\lor} Q)))$
71	6 69 70	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to (p \in M (X \underset{˙}{\lor} Q) \leftrightarrow (p \in A \land p \leq_{K} (X \underset{˙}{\lor} Q)))$
72	71	adantr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to (p \in M (X \underset{˙}{\lor} Q) \leftrightarrow (p \in A \land p \leq_{K} (X \underset{˙}{\lor} Q)))$
73	1 3 4	pmapssat	$⊢ (K \in HL \land X \in B) \to M (X) \subseteq A$
74	73	3adant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (X) \subseteq A$
75	66 74 10	3jca	$⊢ (K \in HL \land X \in B \land Q \in A) \to (K \in Lat \land M (X) \subseteq A \land M (Q) \subseteq A)$
76	75	adantr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to (K \in Lat \land M (X) \subseteq A \land M (Q) \subseteq A)$
77	1 17 4	pmapeq0	$⊢ (K \in HL \land X \in B) \to (M (X) = \emptyset \leftrightarrow X = 0. (K))$
78	77	3adant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to (M (X) = \emptyset \leftrightarrow X = 0. (K))$
79	78	necon3bid	$⊢ (K \in HL \land X \in B \land Q \in A) \to (M (X) \neq \emptyset \leftrightarrow X \neq 0. (K))$
80	79	biimpar	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to M (X) \neq \emptyset$
81		simp3	$⊢ (K \in HL \land X \in B \land Q \in A) \to Q \in A$
82	17 3	atn0	$⊢ (K \in AtLat \land Q \in A) \to Q \neq 0. (K)$
83	16 81 82	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to Q \neq 0. (K)$
84	1 17 4	pmapeq0	$⊢ (K \in HL \land Q \in B) \to (M (Q) = \emptyset \leftrightarrow Q = 0. (K))$
85	6 8 84	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to (M (Q) = \emptyset \leftrightarrow Q = 0. (K))$
86	85	necon3bid	$⊢ (K \in HL \land X \in B \land Q \in A) \to (M (Q) \neq \emptyset \leftrightarrow Q \neq 0. (K))$
87	83 86	mpbird	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q) \neq \emptyset$
88	87	adantr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to M (Q) \neq \emptyset$
89	40 2 3 5	elpaddn0	$⊢ ((K \in Lat \land M (X) \subseteq A \land M (Q) \subseteq A) \land (M (X) \neq \emptyset \land M (Q) \neq \emptyset)) \to (p \in (M (X) \underset{˙}{+} M (Q)) \leftrightarrow (p \in A \land \exists q \in M (X) \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r)))$
90	76 80 88 89	syl12anc	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to (p \in (M (X) \underset{˙}{+} M (Q)) \leftrightarrow (p \in A \land \exists q \in M (X) \exists r \in M (Q) p \leq_{K} (q \underset{˙}{\lor} r)))$
91	64 72 90	3imtr4d	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to (p \in M (X \underset{˙}{\lor} Q) \to p \in (M (X) \underset{˙}{+} M (Q)))$
92	91	ssrdv	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to M (X \underset{˙}{\lor} Q) \subseteq M (X) \underset{˙}{+} M (Q)$
93	1 2 4 5	pmapjoin	$⊢ (K \in Lat \land X \in B \land Q \in B) \to M (X) \underset{˙}{+} M (Q) \subseteq M (X \underset{˙}{\lor} Q)$
94	66 67 8 93	syl3anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (X) \underset{˙}{+} M (Q) \subseteq M (X \underset{˙}{\lor} Q)$
95	94	adantr	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to M (X) \underset{˙}{+} M (Q) \subseteq M (X \underset{˙}{\lor} Q)$
96	92 95	eqssd	$⊢ ((K \in HL \land X \in B \land Q \in A) \land X \neq 0. (K)) \to M (X \underset{˙}{\lor} Q) = M (X) \underset{˙}{+} M (Q)$
97	29 96	pm2.61dane	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (X \underset{˙}{\lor} Q) = M (X) \underset{˙}{+} M (Q)$

Metamath Proof Explorer

Theorem pmapjat1

Proof