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 40292

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 6846.) (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 40179	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ 𝐴)
5	2, 3	paddunssN 40173	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇))
6		paddun.o	. . . 4 ⊢ ⊥ = (⊥_𝑃‘𝐾)
7	2, 6	polcon3N 40282	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
8	1, 4, 5, 7	syl3anc 1374	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
9		hlclat 39723	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
10	9	3ad2ant1 1134	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat)
11		unss 4144	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴)
12	11	biimpi 216	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
13	12	3adant1 1131	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
14		eqid 2737	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
15	14, 2	atssbase 39655	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
16	13, 15	sstrdi 3948	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾))
17		eqid 2737	. . . . . . . . 9 ⊢ (lub‘𝐾) = (lub‘𝐾)
18	14, 17	clatlubcl 18438	. . . . . . . 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 40125	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
22	1, 19, 21	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
23	2, 6	polssatN 40273	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
24	23	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
25	2, 6	polssatN 40273	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑆) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
26	1, 24, 25	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
27	2, 6	polssatN 40273	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
28	27	3adant2 1132	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
29	2, 6	polssatN 40273	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
30	1, 28, 29	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
31	1, 26, 30	3jca 1129	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴))
32	2, 6	2polssN 40280	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
33	32	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
34	2, 6	2polssN 40280	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
35	34	3adant2 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
36	33, 35	jca 511	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))))
37	2, 3	paddss12 40184	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴) → ((𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇)))))
38	31, 36, 37	sylc 65	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))))
39	17, 2, 20, 6	2polvalN 40279	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
40	39	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
41	17, 2, 20, 6	2polvalN 40279	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
42	41	3adant2 1132	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
43	40, 42	oveq12d 7386	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
44	38, 43	sseqtrd 3972	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
45		hllat 39728	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
46	45	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ Lat)
47		simp2 1138	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴)
48	47, 15	sstrdi 3948	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾))
49	14, 17	clatlubcl 18438	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
50	10, 48, 49	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
51		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴)
52	51, 15	sstrdi 3948	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾))
53	14, 17	clatlubcl 18438	. . . . . . . . . 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 40217	. . . . . . . . 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 3946	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
59	14, 55, 17	lubun 18450	. . . . . . . . 9 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
60	10, 48, 52, 59	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
61	60	fveq2d 6846	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
62	58, 61	sseqtrrd 3973	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
63		eqid 2737	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
64	14, 63, 17	lubss 18448	. . . . . 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 3948	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (Base‘𝐾))
67	14, 17	clatlubcl 18438	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 + 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
68	10, 66, 67	syl2anc 585	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
69	14, 17	clatlubcl 18438	. . . . . . 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 40126	. . . . . 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 40279	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
75	1, 4, 74	syl2anc 585	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
76	17, 2, 20, 6	2polvalN 40279	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
77	1, 13, 76	syl2anc 585	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
78	17, 2, 20	2pmaplubN 40291	. . . . . 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 3991	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))))
82	2, 6	2polcon4bN 40283	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
83	1, 4, 13, 82	syl3anc 1374	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
84	81, 83	mpbid 232	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))
85	8, 84	eqssd 3953	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∪ cun 3901 ⊆ wss 3903 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 Basecbs 17148 lecple 17196 lubclub 18244 joincjn 18246 Latclat 18366 CLatccla 18433 Atomscatm 39628 HLchlt 39715 pmapcpmap 39862 +_𝑃cpadd 40160 ⊥_𝑃cpolN 40267

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 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

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 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-1st 7943 df-2nd 7944 df-proset 18229 df-poset 18248 df-plt 18263 df-lub 18279 df-glb 18280 df-join 18281 df-meet 18282 df-p0 18358 df-p1 18359 df-lat 18367 df-clat 18434 df-oposet 39541 df-ol 39543 df-oml 39544 df-covers 39631 df-ats 39632 df-atl 39663 df-cvlat 39687 df-hlat 39716 df-psubsp 39868 df-pmap 39869 df-padd 40161 df-polarityN 40268

This theorem is referenced by: poldmj1N 40293

W3C validator