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 40373

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 6845.) (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 40260	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ 𝐴)
5	2, 3	paddunssN 40254	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇))
6		paddun.o	. . . 4 ⊢ ⊥ = (⊥_𝑃‘𝐾)
7	2, 6	polcon3N 40363	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
8	1, 4, 5, 7	syl3anc 1374	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
9		hlclat 39804	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
10	9	3ad2ant1 1134	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat)
11		unss 4131	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴)
12	11	biimpi 216	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
13	12	3adant1 1131	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
14		eqid 2737	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
15	14, 2	atssbase 39736	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
16	13, 15	sstrdi 3935	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾))
17		eqid 2737	. . . . . . . . 9 ⊢ (lub‘𝐾) = (lub‘𝐾)
18	14, 17	clatlubcl 18469	. . . . . . . 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 40206	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
22	1, 19, 21	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
23	2, 6	polssatN 40354	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
24	23	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
25	2, 6	polssatN 40354	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑆) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
26	1, 24, 25	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
27	2, 6	polssatN 40354	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
28	27	3adant2 1132	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
29	2, 6	polssatN 40354	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
30	1, 28, 29	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
31	1, 26, 30	3jca 1129	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴))
32	2, 6	2polssN 40361	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
33	32	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
34	2, 6	2polssN 40361	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
35	34	3adant2 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
36	33, 35	jca 511	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))))
37	2, 3	paddss12 40265	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴) → ((𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇)))))
38	31, 36, 37	sylc 65	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))))
39	17, 2, 20, 6	2polvalN 40360	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
40	39	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
41	17, 2, 20, 6	2polvalN 40360	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
42	41	3adant2 1132	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
43	40, 42	oveq12d 7385	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
44	38, 43	sseqtrd 3959	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
45		hllat 39809	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
46	45	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ Lat)
47		simp2 1138	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴)
48	47, 15	sstrdi 3935	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾))
49	14, 17	clatlubcl 18469	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
50	10, 48, 49	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
51		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴)
52	51, 15	sstrdi 3935	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾))
53	14, 17	clatlubcl 18469	. . . . . . . . . 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 40298	. . . . . . . . 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 3933	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
59	14, 55, 17	lubun 18481	. . . . . . . . 9 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
60	10, 48, 52, 59	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
61	60	fveq2d 6845	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
62	58, 61	sseqtrrd 3960	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
63		eqid 2737	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
64	14, 63, 17	lubss 18479	. . . . . 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 3935	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (Base‘𝐾))
67	14, 17	clatlubcl 18469	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 + 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
68	10, 66, 67	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
69	14, 17	clatlubcl 18469	. . . . . . 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 40207	. . . . . 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 40360	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
75	1, 4, 74	syl2anc 585	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
76	17, 2, 20, 6	2polvalN 40360	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
77	1, 13, 76	syl2anc 585	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
78	17, 2, 20	2pmaplubN 40372	. . . . . 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 3978	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))))
82	2, 6	2polcon4bN 40364	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
83	1, 4, 13, 82	syl3anc 1374	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
84	81, 83	mpbid 232	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))
85	8, 84	eqssd 3940	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∪ cun 3888 ⊆ wss 3890 class class class wbr 5086 ‘cfv 6499 (class class class)co 7367 Basecbs 17179 lecple 17227 lubclub 18275 joincjn 18277 Latclat 18397 CLatccla 18464 Atomscatm 39709 HLchlt 39796 pmapcpmap 39943 +_𝑃cpadd 40241 ⊥_𝑃cpolN 40348

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 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689

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 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-1st 7942 df-2nd 7943 df-proset 18260 df-poset 18279 df-plt 18294 df-lub 18310 df-glb 18311 df-join 18312 df-meet 18313 df-p0 18389 df-p1 18390 df-lat 18398 df-clat 18465 df-oposet 39622 df-ol 39624 df-oml 39625 df-covers 39712 df-ats 39713 df-atl 39744 df-cvlat 39768 df-hlat 39797 df-psubsp 39949 df-pmap 39950 df-padd 40242 df-polarityN 40349

This theorem is referenced by: poldmj1N 40374

W3C validator