pmapjoin

Description: The projective map of the join of two lattice elements. Part of Equation 15.5.3 of MaedaMaeda p. 63. (Contributed by NM, 27-Jan-2012)

	Ref	Expression
Hypotheses	pmapjoin.b	$⊢ B = {Base}_{K}$
	pmapjoin.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmapjoin.m	$⊢ M = pmap (K)$
	pmapjoin.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmapjoin	$⊢ (K \in Lat \land X \in B \land Y \in B) \to M (X) \underset{˙}{+} M (Y) \subseteq M (X \underset{˙}{\lor} Y)$

Proof

Step	Hyp	Ref	Expression
1		pmapjoin.b	$⊢ B = {Base}_{K}$
2		pmapjoin.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pmapjoin.m	$⊢ M = pmap (K)$
4		pmapjoin.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		simpl	$⊢ (p \in Atoms (K) \land p \leq_{K} X) \to p \in Atoms (K)$
6	5	a1i	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land p \leq_{K} X) \to p \in Atoms (K))$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	1 7	atbase	$⊢ p \in Atoms (K) \to p \in B$
9		eqid	$⊢ \leq_{K} = \leq_{K}$
10	1 9 2	latlej1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
11	10	adantr	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
12		simpl1	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to K \in Lat$
13		simpr	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to p \in B$
14		simpl2	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to X \in B$
15	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
16	15	adantr	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to X \underset{˙}{\lor} Y \in B$
17	1 9	lattr	$⊢ (K \in Lat \land (p \in B \land X \in B \land X \underset{˙}{\lor} Y \in B)) \to ((p \leq_{K} X \land X \leq_{K} (X \underset{˙}{\lor} Y)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
18	12 13 14 16 17	syl13anc	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to ((p \leq_{K} X \land X \leq_{K} (X \underset{˙}{\lor} Y)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
19	11 18	mpan2d	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to (p \leq_{K} X \to p \leq_{K} (X \underset{˙}{\lor} Y))$
20	19	expimpd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in B \land p \leq_{K} X) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
21	8 20	sylani	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land p \leq_{K} X) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
22	6 21	jcad	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land p \leq_{K} X) \to (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
23		simpl	$⊢ (p \in Atoms (K) \land p \leq_{K} Y) \to p \in Atoms (K)$
24	23	a1i	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land p \leq_{K} Y) \to p \in Atoms (K))$
25	1 9 2	latlej2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to Y \leq_{K} (X \underset{˙}{\lor} Y)$
26	25	adantr	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to Y \leq_{K} (X \underset{˙}{\lor} Y)$
27		simpl3	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to Y \in B$
28	1 9	lattr	$⊢ (K \in Lat \land (p \in B \land Y \in B \land X \underset{˙}{\lor} Y \in B)) \to ((p \leq_{K} Y \land Y \leq_{K} (X \underset{˙}{\lor} Y)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
29	12 13 27 16 28	syl13anc	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to ((p \leq_{K} Y \land Y \leq_{K} (X \underset{˙}{\lor} Y)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
30	26 29	mpan2d	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to (p \leq_{K} Y \to p \leq_{K} (X \underset{˙}{\lor} Y))$
31	30	expimpd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in B \land p \leq_{K} Y) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
32	8 31	sylani	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land p \leq_{K} Y) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
33	24 32	jcad	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land p \leq_{K} Y) \to (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
34	22 33	jaod	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (((p \in Atoms (K) \land p \leq_{K} X) \lor (p \in Atoms (K) \land p \leq_{K} Y)) \to (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
35		simpl	$⊢ (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r)) \to p \in Atoms (K)$
36	35	a1i	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r)) \to p \in Atoms (K))$
37	1 9 7 3	elpmap	$⊢ (K \in Lat \land X \in B) \to (q \in M (X) \leftrightarrow (q \in Atoms (K) \land q \leq_{K} X))$
38	37	3adant3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (q \in M (X) \leftrightarrow (q \in Atoms (K) \land q \leq_{K} X))$
39	1 9 7 3	elpmap	$⊢ (K \in Lat \land Y \in B) \to (r \in M (Y) \leftrightarrow (r \in Atoms (K) \land r \leq_{K} Y))$
40	39	3adant2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (r \in M (Y) \leftrightarrow (r \in Atoms (K) \land r \leq_{K} Y))$
41	38 40	anbi12d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((q \in M (X) \land r \in M (Y)) \leftrightarrow ((q \in Atoms (K) \land q \leq_{K} X) \land (r \in Atoms (K) \land r \leq_{K} Y)))$
42		an4	$⊢ ((q \in Atoms (K) \land q \leq_{K} X) \land (r \in Atoms (K) \land r \leq_{K} Y)) \leftrightarrow ((q \in Atoms (K) \land r \in Atoms (K)) \land (q \leq_{K} X \land r \leq_{K} Y))$
43	41 42	syl6bb	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((q \in M (X) \land r \in M (Y)) \leftrightarrow ((q \in Atoms (K) \land r \in Atoms (K)) \land (q \leq_{K} X \land r \leq_{K} Y)))$
44	43	adantr	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to ((q \in M (X) \land r \in M (Y)) \leftrightarrow ((q \in Atoms (K) \land r \in Atoms (K)) \land (q \leq_{K} X \land r \leq_{K} Y)))$
45	1 7	atbase	$⊢ q \in Atoms (K) \to q \in B$
46	1 7	atbase	$⊢ r \in Atoms (K) \to r \in B$
47	45 46	anim12i	$⊢ (q \in Atoms (K) \land r \in Atoms (K)) \to (q \in B \land r \in B)$
48		simpll1	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to K \in Lat$
49		simprl	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to q \in B$
50		simpll2	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to X \in B$
51		simprr	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to r \in B$
52		simpll3	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to Y \in B$
53	1 9 2	latjlej12	$⊢ (K \in Lat \land (q \in B \land X \in B) \land (r \in B \land Y \in B)) \to ((q \leq_{K} X \land r \leq_{K} Y) \to (q \underset{˙}{\lor} r) \leq_{K} (X \underset{˙}{\lor} Y))$
54	48 49 50 51 52 53	syl122anc	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to ((q \leq_{K} X \land r \leq_{K} Y) \to (q \underset{˙}{\lor} r) \leq_{K} (X \underset{˙}{\lor} Y))$
55		simplr	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to p \in B$
56	1 2	latjcl	$⊢ (K \in Lat \land q \in B \land r \in B) \to q \underset{˙}{\lor} r \in B$
57	48 49 51 56	syl3anc	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to q \underset{˙}{\lor} r \in B$
58	15	ad2antrr	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to X \underset{˙}{\lor} Y \in B$
59	1 9	lattr	$⊢ (K \in Lat \land (p \in B \land q \underset{˙}{\lor} r \in B \land X \underset{˙}{\lor} Y \in B)) \to ((p \leq_{K} (q \underset{˙}{\lor} r) \land (q \underset{˙}{\lor} r) \leq_{K} (X \underset{˙}{\lor} Y)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
60	48 55 57 58 59	syl13anc	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to ((p \leq_{K} (q \underset{˙}{\lor} r) \land (q \underset{˙}{\lor} r) \leq_{K} (X \underset{˙}{\lor} Y)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
61	60	expcomd	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to ((q \underset{˙}{\lor} r) \leq_{K} (X \underset{˙}{\lor} Y) \to (p \leq_{K} (q \underset{˙}{\lor} r) \to p \leq_{K} (X \underset{˙}{\lor} Y)))$
62	54 61	syld	$⊢ (((K \in Lat \land X \in B \land Y \in B) \land p \in B) \land (q \in B \land r \in B)) \to ((q \leq_{K} X \land r \leq_{K} Y) \to (p \leq_{K} (q \underset{˙}{\lor} r) \to p \leq_{K} (X \underset{˙}{\lor} Y)))$
63	62	expimpd	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to (((q \in B \land r \in B) \land (q \leq_{K} X \land r \leq_{K} Y)) \to (p \leq_{K} (q \underset{˙}{\lor} r) \to p \leq_{K} (X \underset{˙}{\lor} Y)))$
64	47 63	sylani	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to (((q \in Atoms (K) \land r \in Atoms (K)) \land (q \leq_{K} X \land r \leq_{K} Y)) \to (p \leq_{K} (q \underset{˙}{\lor} r) \to p \leq_{K} (X \underset{˙}{\lor} Y)))$
65	44 64	sylbid	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to ((q \in M (X) \land r \in M (Y)) \to (p \leq_{K} (q \underset{˙}{\lor} r) \to p \leq_{K} (X \underset{˙}{\lor} Y)))$
66	65	rexlimdvv	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land p \in B) \to (\exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
67	66	expimpd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in B \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
68	8 67	sylani	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r)) \to p \leq_{K} (X \underset{˙}{\lor} Y))$
69	36 68	jcad	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r)) \to (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
70	34 69	jaod	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((((p \in Atoms (K) \land p \leq_{K} X) \lor (p \in Atoms (K) \land p \leq_{K} Y)) \lor (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r))) \to (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
71		simp1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to K \in Lat$
72	1 7 3	pmapssat	$⊢ (K \in Lat \land X \in B) \to M (X) \subseteq Atoms (K)$
73	72	3adant3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to M (X) \subseteq Atoms (K)$
74	1 7 3	pmapssat	$⊢ (K \in Lat \land Y \in B) \to M (Y) \subseteq Atoms (K)$
75	74	3adant2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to M (Y) \subseteq Atoms (K)$
76	9 2 7 4	elpadd	$⊢ (K \in Lat \land M (X) \subseteq Atoms (K) \land M (Y) \subseteq Atoms (K)) \to (p \in (M (X) \underset{˙}{+} M (Y)) \leftrightarrow ((p \in M (X) \lor p \in M (Y)) \lor (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r))))$
77	71 73 75 76	syl3anc	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (p \in (M (X) \underset{˙}{+} M (Y)) \leftrightarrow ((p \in M (X) \lor p \in M (Y)) \lor (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r))))$
78	1 9 7 3	elpmap	$⊢ (K \in Lat \land X \in B) \to (p \in M (X) \leftrightarrow (p \in Atoms (K) \land p \leq_{K} X))$
79	78	3adant3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (p \in M (X) \leftrightarrow (p \in Atoms (K) \land p \leq_{K} X))$
80	1 9 7 3	elpmap	$⊢ (K \in Lat \land Y \in B) \to (p \in M (Y) \leftrightarrow (p \in Atoms (K) \land p \leq_{K} Y))$
81	80	3adant2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (p \in M (Y) \leftrightarrow (p \in Atoms (K) \land p \leq_{K} Y))$
82	79 81	orbi12d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((p \in M (X) \lor p \in M (Y)) \leftrightarrow ((p \in Atoms (K) \land p \leq_{K} X) \lor (p \in Atoms (K) \land p \leq_{K} Y)))$
83	82	orbi1d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (((p \in M (X) \lor p \in M (Y)) \lor (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r))) \leftrightarrow (((p \in Atoms (K) \land p \leq_{K} X) \lor (p \in Atoms (K) \land p \leq_{K} Y)) \lor (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r))))$
84	77 83	bitrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (p \in (M (X) \underset{˙}{+} M (Y)) \leftrightarrow (((p \in Atoms (K) \land p \leq_{K} X) \lor (p \in Atoms (K) \land p \leq_{K} Y)) \lor (p \in Atoms (K) \land \exists q \in M (X) \exists r \in M (Y) p \leq_{K} (q \underset{˙}{\lor} r))))$
85	1 9 7 3	elpmap	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B) \to (p \in M (X \underset{˙}{\lor} Y) \leftrightarrow (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
86	71 15 85	syl2anc	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (p \in M (X \underset{˙}{\lor} Y) \leftrightarrow (p \in Atoms (K) \land p \leq_{K} (X \underset{˙}{\lor} Y)))$
87	70 84 86	3imtr4d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (p \in (M (X) \underset{˙}{+} M (Y)) \to p \in M (X \underset{˙}{\lor} Y))$
88	87	ssrdv	$⊢ (K \in Lat \land X \in B \land Y \in B) \to M (X) \underset{˙}{+} M (Y) \subseteq M (X \underset{˙}{\lor} Y)$

Metamath Proof Explorer

Theorem pmapjoin

Proof