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 39921

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 6862.) (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 1136	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ HL)
2		paddun.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
3		paddun.p	. . . 4 ⊢ + = (+_𝑃‘𝐾)
4	2, 3	paddssat 39808	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ 𝐴)
5	2, 3	paddunssN 39802	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇))
6		paddun.o	. . . 4 ⊢ ⊥ = (⊥_𝑃‘𝐾)
7	2, 6	polcon3N 39911	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
8	1, 4, 5, 7	syl3anc 1373	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
9		hlclat 39351	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
10	9	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat)
11		unss 4153	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴)
12	11	biimpi 216	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
13	12	3adant1 1130	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
14		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
15	14, 2	atssbase 39283	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
16	13, 15	sstrdi 3959	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾))
17		eqid 2729	. . . . . . . . 9 ⊢ (lub‘𝐾) = (lub‘𝐾)
18	14, 17	clatlubcl 18462	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾))
19	10, 16, 18	syl2anc 584	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾))
20		eqid 2729	. . . . . . . 8 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
21	14, 20	pmapssbaN 39754	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
22	1, 19, 21	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
23	2, 6	polssatN 39902	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
24	23	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
25	2, 6	polssatN 39902	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑆) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
26	1, 24, 25	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
27	2, 6	polssatN 39902	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
28	27	3adant2 1131	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
29	2, 6	polssatN 39902	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
30	1, 28, 29	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
31	1, 26, 30	3jca 1128	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴))
32	2, 6	2polssN 39909	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
33	32	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
34	2, 6	2polssN 39909	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
35	34	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
36	33, 35	jca 511	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))))
37	2, 3	paddss12 39813	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴) → ((𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇)))))
38	31, 36, 37	sylc 65	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))))
39	17, 2, 20, 6	2polvalN 39908	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
40	39	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
41	17, 2, 20, 6	2polvalN 39908	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
42	41	3adant2 1131	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
43	40, 42	oveq12d 7405	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
44	38, 43	sseqtrd 3983	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
45		hllat 39356	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
46	45	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ Lat)
47		simp2 1137	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴)
48	47, 15	sstrdi 3959	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾))
49	14, 17	clatlubcl 18462	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
50	10, 48, 49	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
51		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴)
52	51, 15	sstrdi 3959	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾))
53	14, 17	clatlubcl 18462	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾))
54	10, 52, 53	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾))
55		eqid 2729	. . . . . . . . . 10 ⊢ (join‘𝐾) = (join‘𝐾)
56	14, 55, 20, 3	pmapjoin 39846	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾)) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
57	46, 50, 54, 56	syl3anc 1373	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
58	44, 57	sstrd 3957	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
59	14, 55, 17	lubun 18474	. . . . . . . . 9 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
60	10, 48, 52, 59	syl3anc 1373	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
61	60	fveq2d 6862	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
62	58, 61	sseqtrrd 3984	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
63		eqid 2729	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
64	14, 63, 17	lubss 18472	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾) ∧ (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) → ((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))
65	10, 22, 62, 64	syl3anc 1373	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇))(le‘𝐾)((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))))
66	4, 15	sstrdi 3959	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (Base‘𝐾))
67	14, 17	clatlubcl 18462	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 + 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
68	10, 66, 67	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
69	14, 17	clatlubcl 18462	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾))
70	10, 22, 69	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇)))) ∈ (Base‘𝐾))
71	14, 63, 20	pmaple 39755	. . . . . 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 1373	. . . . 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 39908	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
75	1, 4, 74	syl2anc 584	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
76	17, 2, 20, 6	2polvalN 39908	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
77	1, 13, 76	syl2anc 584	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
78	17, 2, 20	2pmaplubN 39920	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
79	1, 13, 78	syl2anc 584	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
80	77, 79	eqtr4d 2767	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))))
81	73, 75, 80	3sstr4d 4002	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))))
82	2, 6	2polcon4bN 39912	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
83	1, 4, 13, 82	syl3anc 1373	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
84	81, 83	mpbid 232	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))
85	8, 84	eqssd 3964	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∪ cun 3912 ⊆ wss 3914 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 Basecbs 17179 lecple 17227 lubclub 18270 joincjn 18272 Latclat 18390 CLatccla 18457 Atomscatm 39256 HLchlt 39343 pmapcpmap 39491 +_𝑃cpadd 39789 ⊥_𝑃cpolN 39896

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-1st 7968 df-2nd 7969 df-proset 18255 df-poset 18274 df-plt 18289 df-lub 18305 df-glb 18306 df-join 18307 df-meet 18308 df-p0 18384 df-p1 18385 df-lat 18391 df-clat 18458 df-oposet 39169 df-ol 39171 df-oml 39172 df-covers 39259 df-ats 39260 df-atl 39291 df-cvlat 39315 df-hlat 39344 df-psubsp 39497 df-pmap 39498 df-padd 39790 df-polarityN 39897

This theorem is referenced by: poldmj1N 39922

W3C validator