paddunN - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > paddunN		Structured version Visualization version GIF version

Theorem paddunN 40224

Description: The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d 6839.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
paddun.a	⊢ 𝐴 = (Atoms‘𝐾)
paddun.p	⊢ + = (+_𝑃‘𝐾)
paddun.o	⊢ ⊥ = (⊥_𝑃‘𝐾)

**Assertion**
Ref	Expression
paddunN	⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))

**Proof of Theorem paddunN**
Step	Hyp	Ref	Expression
1		simp1 1137	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ HL)
2		paddun.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
3		paddun.p	. . . 4 ⊢ + = (+_𝑃‘𝐾)
4	2, 3	paddssat 40111	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ 𝐴)
5	2, 3	paddunssN 40105	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇))
6		paddun.o	. . . 4 ⊢ ⊥ = (⊥_𝑃‘𝐾)
7	2, 6	polcon3N 40214	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
8	1, 4, 5, 7	syl3anc 1374	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
9		hlclat 39655	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
10	9	3ad2ant1 1134	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat)
11		unss 4143	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴)
12	11	biimpi 216	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
13	12	3adant1 1131	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
14		eqid 2737	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
15	14, 2	atssbase 39587	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
16	13, 15	sstrdi 3947	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾))
17		eqid 2737	. . . . . . . . 9 ⊢ (lub‘𝐾) = (lub‘𝐾)
18	14, 17	clatlubcl 18430	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾))
19	10, 16, 18	syl2anc 585	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾))
20		eqid 2737	. . . . . . . 8 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
21	14, 20	pmapssbaN 40057	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
22	1, 19, 21	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
23	2, 6	polssatN 40205	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
24	23	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
25	2, 6	polssatN 40205	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑆) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
26	1, 24, 25	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
27	2, 6	polssatN 40205	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
28	27	3adant2 1132	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
29	2, 6	polssatN 40205	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
30	1, 28, 29	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
31	1, 26, 30	3jca 1129	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴))
32	2, 6	2polssN 40212	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
33	32	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
34	2, 6	2polssN 40212	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
35	34	3adant2 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
36	33, 35	jca 511	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))))
37	2, 3	paddss12 40116	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴) → ((𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇)))))
38	31, 36, 37	sylc 65	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))))
39	17, 2, 20, 6	2polvalN 40211	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
40	39	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
41	17, 2, 20, 6	2polvalN 40211	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
42	41	3adant2 1132	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
43	40, 42	oveq12d 7378	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
44	38, 43	sseqtrd 3971	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
45		hllat 39660	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
46	45	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ Lat)
47		simp2 1138	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴)
48	47, 15	sstrdi 3947	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾))
49	14, 17	clatlubcl 18430	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
50	10, 48, 49	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
51		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴)
52	51, 15	sstrdi 3947	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾))
53	14, 17	clatlubcl 18430	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾))
54	10, 52, 53	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾))
55		eqid 2737	. . . . . . . . . 10 ⊢ (join‘𝐾) = (join‘𝐾)
56	14, 55, 20, 3	pmapjoin 40149	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
57	46, 50, 54, 56	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
58	44, 57	sstrd 3945	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
59	14, 55, 17	lubun 18442	. . . . . . . . 9 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
60	10, 48, 52, 59	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
61	60	fveq2d 6839	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
62	58, 61	sseqtrrd 3972	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
63		eqid 2737	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
64	14, 63, 17	lubss 18440	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾) ∧ (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) → ((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))
65	10, 22, 62, 64	syl3anc 1374	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))
66	4, 15	sstrdi 3947	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (Base‘𝐾))
67	14, 17	clatlubcl 18430	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 + 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
68	10, 66, 67	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
69	14, 17	clatlubcl 18430	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾))
70	10, 22, 69	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾))
71	14, 63, 20	pmaple 40058	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾)) → (((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ↔ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))))
72	1, 68, 70, 71	syl3anc 1374	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ↔ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))))
73	65, 72	mpbid 232	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))))
74	17, 2, 20, 6	2polvalN 40211	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
75	1, 4, 74	syl2anc 585	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
76	17, 2, 20, 6	2polvalN 40211	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
77	1, 13, 76	syl2anc 585	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
78	17, 2, 20	2pmaplubN 40223	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
79	1, 13, 78	syl2anc 585	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
80	77, 79	eqtr4d 2775	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))))
81	73, 75, 80	3sstr4d 3990	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))))
82	2, 6	2polcon4bN 40215	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
83	1, 4, 13, 82	syl3anc 1374	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
84	81, 83	mpbid 232	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))
85	8, 84	eqssd 3952	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∪ cun 3900 ⊆ wss 3902 class class class wbr 5099 ‘cfv 6493 (class class class)co 7360 Basecbs 17140 lecple 17188 lubclub 18236 joincjn 18238 Latclat 18358 CLatccla 18425 Atomscatm 39560 HLchlt 39647 pmapcpmap 39794 +_𝑃cpadd 40092 ⊥_𝑃cpolN 40199

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4949 df-iin 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-1st 7935 df-2nd 7936 df-proset 18221 df-poset 18240 df-plt 18255 df-lub 18271 df-glb 18272 df-join 18273 df-meet 18274 df-p0 18350 df-p1 18351 df-lat 18359 df-clat 18426 df-oposet 39473 df-ol 39475 df-oml 39476 df-covers 39563 df-ats 39564 df-atl 39595 df-cvlat 39619 df-hlat 39648 df-psubsp 39800 df-pmap 39801 df-padd 40093 df-polarityN 40200

This theorem is referenced by: poldmj1N 40225

W3C validator