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 39951

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 6885.) (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 39838	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ 𝐴)
5	2, 3	paddunssN 39832	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇))
6		paddun.o	. . . 4 ⊢ ⊥ = (⊥_𝑃‘𝐾)
7	2, 6	polcon3N 39941	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ (𝑆 + 𝑇)) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
8	1, 4, 5, 7	syl3anc 1373	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) ⊆ ( ⊥ ‘(𝑆 ∪ 𝑇)))
9		hlclat 39381	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
10	9	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ CLat)
11		unss 4170	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) ↔ (𝑆 ∪ 𝑇) ⊆ 𝐴)
12	11	biimpi 216	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
13	12	3adant1 1130	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ 𝐴)
14		eqid 2736	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
15	14, 2	atssbase 39313	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
16	13, 15	sstrdi 3976	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾))
17		eqid 2736	. . . . . . . . 9 ⊢ (lub‘𝐾) = (lub‘𝐾)
18	14, 17	clatlubcl 18518	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 ∪ 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾))
19	10, 16, 18	syl2anc 584	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾))
20		eqid 2736	. . . . . . . 8 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
21	14, 20	pmapssbaN 39784	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
22	1, 19, 21	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) ⊆ (Base‘𝐾))
23	2, 6	polssatN 39932	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
24	23	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑆) ⊆ 𝐴)
25	2, 6	polssatN 39932	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑆) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
26	1, 24, 25	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴)
27	2, 6	polssatN 39932	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
28	27	3adant2 1131	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘𝑇) ⊆ 𝐴)
29	2, 6	polssatN 39932	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
30	1, 28, 29	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴)
31	1, 26, 30	3jca 1128	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴))
32	2, 6	2polssN 39939	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
33	32	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
34	2, 6	2polssN 39939	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
35	34	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇)))
36	33, 35	jca 511	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))))
37	2, 3	paddss12 39843	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑇)) ⊆ 𝐴) → ((𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)) ∧ 𝑇 ⊆ ( ⊥ ‘( ⊥ ‘𝑇))) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇)))))
38	31, 36, 37	sylc 65	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))))
39	17, 2, 20, 6	2polvalN 39938	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
40	39	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑆)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)))
41	17, 2, 20, 6	2polvalN 39938	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
42	41	3adant2 1131	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑇)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇)))
43	40, 42	oveq12d 7428	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑆)) + ( ⊥ ‘( ⊥ ‘𝑇))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
44	38, 43	sseqtrd 4000	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (((pmap‘𝐾)‘((lub‘𝐾)‘𝑆)) + ((pmap‘𝐾)‘((lub‘𝐾)‘𝑇))))
45		hllat 39386	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
46	45	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝐾 ∈ Lat)
47		simp2 1137	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ 𝐴)
48	47, 15	sstrdi 3976	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑆 ⊆ (Base‘𝐾))
49	14, 17	clatlubcl 18518	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
50	10, 48, 49	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑆) ∈ (Base‘𝐾))
51		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ 𝐴)
52	51, 15	sstrdi 3976	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → 𝑇 ⊆ (Base‘𝐾))
53	14, 17	clatlubcl 18518	. . . . . . . . . 10 ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾))
54	10, 52, 53	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘𝑇) ∈ (Base‘𝐾))
55		eqid 2736	. . . . . . . . . 10 ⊢ (join‘𝐾) = (join‘𝐾)
56	14, 55, 20, 3	pmapjoin 39876	. . . . . . . . 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 3974	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
59	14, 55, 17	lubun 18530	. . . . . . . . 9 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ (Base‘𝐾) ∧ 𝑇 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
60	10, 48, 52, 59	syl3anc 1373	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 ∪ 𝑇)) = (((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇)))
61	60	fveq2d 6885	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑆)(join‘𝐾)((lub‘𝐾)‘𝑇))))
62	58, 61	sseqtrrd 4001	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
63		eqid 2736	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
64	14, 63, 17	lubss 18528	. . . . . 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 3976	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (𝑆 + 𝑇) ⊆ (Base‘𝐾))
67	14, 17	clatlubcl 18518	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ (𝑆 + 𝑇) ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
68	10, 66, 67	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ((lub‘𝐾)‘(𝑆 + 𝑇)) ∈ (Base‘𝐾))
69	14, 17	clatlubcl 18518	. . . . . . 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 39785	. . . . . 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 39938	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
75	1, 4, 74	syl2anc 584	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 + 𝑇))))
76	17, 2, 20, 6	2polvalN 39938	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
77	1, 13, 76	syl2anc 584	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))
78	17, 2, 20	2pmaplubN 39950	. . . . . 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 2774	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) = ((pmap‘𝐾)‘((lub‘𝐾)‘((pmap‘𝐾)‘((lub‘𝐾)‘(𝑆 ∪ 𝑇))))))
81	73, 75, 80	3sstr4d 4019	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))))
82	2, 6	2polcon4bN 39942	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑆 + 𝑇) ⊆ 𝐴 ∧ (𝑆 ∪ 𝑇) ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
83	1, 4, 13, 82	syl3anc 1373	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘(𝑆 + 𝑇))) ⊆ ( ⊥ ‘( ⊥ ‘(𝑆 ∪ 𝑇))) ↔ ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇))))
84	81, 83	mpbid 232	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 ∪ 𝑇)) ⊆ ( ⊥ ‘(𝑆 + 𝑇)))
85	8, 84	eqssd 3981	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∪ cun 3929 ⊆ wss 3931 class class class wbr 5124 ‘cfv 6536 (class class class)co 7410 Basecbs 17233 lecple 17283 lubclub 18326 joincjn 18328 Latclat 18446 CLatccla 18513 Atomscatm 39286 HLchlt 39373 pmapcpmap 39521 +_𝑃cpadd 39819 ⊥_𝑃cpolN 39926

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 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7993 df-2nd 7994 df-proset 18311 df-poset 18330 df-plt 18345 df-lub 18361 df-glb 18362 df-join 18363 df-meet 18364 df-p0 18440 df-p1 18441 df-lat 18447 df-clat 18514 df-oposet 39199 df-ol 39201 df-oml 39202 df-covers 39289 df-ats 39290 df-atl 39321 df-cvlat 39345 df-hlat 39374 df-psubsp 39527 df-pmap 39528 df-padd 39820 df-polarityN 39927

This theorem is referenced by: poldmj1N 39952

W3C validator