poml4N - Mathbox for Norm Megill

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

Theorem poml4N 40152

Description: Orthomodular law for projective lattices. Lemma 3.3(1) in [Holland95] p. 215. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)

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

**Assertion**
Ref	Expression
poml4N	⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))))

**Proof of Theorem poml4N**
Step	Hyp	Ref	Expression
1		eqcom 2741	. . 3 ⊢ (( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌 ↔ 𝑌 = ( ⊥ ‘( ⊥ ‘𝑌)))
2		eqid 2734	. . . . . . 7 ⊢ (lub‘𝐾) = (lub‘𝐾)
3		poml4.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
4		eqid 2734	. . . . . . 7 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
5		poml4.p	. . . . . . 7 ⊢ ⊥ = (⊥_𝑃‘𝐾)
6	2, 3, 4, 5	2polvalN 40113	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑌)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))
7	6	3adant2 1131	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑌)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))
8	7	eqeq2d 2745	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑌 = ( ⊥ ‘( ⊥ ‘𝑌)) ↔ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
9	8	biimpd 229	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑌 = ( ⊥ ‘( ⊥ ‘𝑌)) → 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
10	1, 9	biimtrid 242	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌 → 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
11		simpl1 1192	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ HL)
12		hloml 39556	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
13	11, 12	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ OML)
14		hlclat 39557	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
15	11, 14	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ CLat)
16		simpl2 1193	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑋 ⊆ 𝐴)
17		eqid 2734	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
18	17, 3	atssbase 39489	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
19	16, 18	sstrdi 3944	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑋 ⊆ (Base‘𝐾))
20	17, 2	clatlubcl 18424	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
21	15, 19, 20	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
22		simpl3 1194	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑌 ⊆ 𝐴)
23	22, 18	sstrdi 3944	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑌 ⊆ (Base‘𝐾))
24	17, 2	clatlubcl 18424	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ 𝑌 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾))
25	15, 23, 24	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾))
26	13, 21, 25	3jca 1128	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (𝐾 ∈ OML ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)))
27		simprl 770	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑋 ⊆ 𝑌)
28		eqid 2734	. . . . . . . 8 ⊢ (le‘𝐾) = (le‘𝐾)
29	17, 28, 2	lubss 18434	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ 𝑌 ⊆ (Base‘𝐾) ∧ 𝑋 ⊆ 𝑌) → ((lub‘𝐾)‘𝑋)(le‘𝐾)((lub‘𝐾)‘𝑌))
30	15, 23, 27, 29	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((lub‘𝐾)‘𝑋)(le‘𝐾)((lub‘𝐾)‘𝑌))
31		eqid 2734	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
32		eqid 2734	. . . . . . 7 ⊢ (oc‘𝐾) = (oc‘𝐾)
33	17, 28, 31, 32	omllaw4 39445	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)) → (((lub‘𝐾)‘𝑋)(le‘𝐾)((lub‘𝐾)‘𝑌) → (((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌)) = ((lub‘𝐾)‘𝑋)))
34	26, 30, 33	sylc 65	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌)) = ((lub‘𝐾)‘𝑋))
35	34	fveq2d 6836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)))
36	2, 32, 3, 4, 5	polval2N 40105	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
37	11, 16, 36	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
38		simprr 772	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))
39	37, 38	ineq12d 4171	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘𝑋) ∩ 𝑌) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
40		hlop 39561	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
41	11, 40	syl 17	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ OP)
42	17, 32	opoccl 39393	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
43	41, 21, 42	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
44	17, 31, 3, 4	pmapmeet 39972	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
45	11, 43, 25, 44	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
46	39, 45	eqtr4d 2772	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘𝑋) ∩ 𝑌) = ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))))
47	46	fveq2d 6836	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) = ( ⊥ ‘((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
48	11	hllatd 39563	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ Lat)
49	17, 31	latmcl 18361	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾))
50	48, 43, 25, 49	syl3anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾))
51	17, 32, 4, 5	polpmapN 40111	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾)) → ( ⊥ ‘((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) = ((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
52	11, 50, 51	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) = ((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
53	47, 52	eqtrd 2769	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) = ((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
54	53, 38	ineq12d 4171	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = (((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
55	17, 32	opoccl 39393	. . . . . . 7 ⊢ ((𝐾 ∈ OP ∧ (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) ∈ (Base‘𝐾))
56	41, 50, 55	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) ∈ (Base‘𝐾))
57	17, 31, 3, 4	pmapmeet 39972	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
58	11, 56, 25, 57	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
59	54, 58	eqtr4d 2772	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))))
60	2, 3, 4, 5	2polvalN 40113	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)))
61	11, 16, 60	syl2anc 584	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘( ⊥ ‘𝑋)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)))
62	35, 59, 61	3eqtr4d 2779	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))
63	62	ex 412	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))))
64	10, 63	sylan2d 605	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∩ cin 3898 ⊆ wss 3899 class class class wbr 5096 ‘cfv 6490 (class class class)co 7356 Basecbs 17134 lecple 17182 occoc 17183 lubclub 18230 meetcmee 18233 Latclat 18352 CLatccla 18419 OPcops 39371 OMLcoml 39374 Atomscatm 39462 HLchlt 39549 pmapcpmap 39696 ⊥_𝑃cpolN 40101

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-iun 4946 df-iin 4947 df-br 5097 df-opab 5159 df-mpt 5178 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-proset 18215 df-poset 18234 df-plt 18249 df-lub 18265 df-glb 18266 df-join 18267 df-meet 18268 df-p0 18344 df-p1 18345 df-lat 18353 df-clat 18420 df-oposet 39375 df-ol 39377 df-oml 39378 df-covers 39465 df-ats 39466 df-atl 39497 df-cvlat 39521 df-hlat 39550 df-pmap 39703 df-polarityN 40102

This theorem is referenced by: poml5N 40153 poml6N 40154 pexmidlem6N 40174

W3C validator