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 37894

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 2745	. . 3 ⊢ (( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌 ↔ 𝑌 = ( ⊥ ‘( ⊥ ‘𝑌)))
2		eqid 2738	. . . . . . 7 ⊢ (lub‘𝐾) = (lub‘𝐾)
3		poml4.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
4		eqid 2738	. . . . . . 7 ⊢ (pmap‘𝐾) = (pmap‘𝐾)
5		poml4.p	. . . . . . 7 ⊢ ⊥ = (⊥_𝑃‘𝐾)
6	2, 3, 4, 5	2polvalN 37855	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑌)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))
7	6	3adant2 1129	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑌)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))
8	7	eqeq2d 2749	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑌 = ( ⊥ ‘( ⊥ ‘𝑌)) ↔ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
9	8	biimpd 228	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑌 = ( ⊥ ‘( ⊥ ‘𝑌)) → 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
10	1, 9	syl5bi 241	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌 → 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
11		simpl1 1189	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ HL)
12		hloml 37298	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
13	11, 12	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ OML)
14		hlclat 37299	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
15	11, 14	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ CLat)
16		simpl2 1190	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑋 ⊆ 𝐴)
17		eqid 2738	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
18	17, 3	atssbase 37231	. . . . . . . . 9 ⊢ 𝐴 ⊆ (Base‘𝐾)
19	16, 18	sstrdi 3929	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑋 ⊆ (Base‘𝐾))
20	17, 2	clatlubcl 18136	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
21	15, 19, 20	syl2anc 583	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾))
22		simpl3 1191	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑌 ⊆ 𝐴)
23	22, 18	sstrdi 3929	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑌 ⊆ (Base‘𝐾))
24	17, 2	clatlubcl 18136	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ 𝑌 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾))
25	15, 23, 24	syl2anc 583	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾))
26	13, 21, 25	3jca 1126	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (𝐾 ∈ OML ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)))
27		simprl 767	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑋 ⊆ 𝑌)
28		eqid 2738	. . . . . . . 8 ⊢ (le‘𝐾) = (le‘𝐾)
29	17, 28, 2	lubss 18146	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ 𝑌 ⊆ (Base‘𝐾) ∧ 𝑋 ⊆ 𝑌) → ((lub‘𝐾)‘𝑋)(le‘𝐾)((lub‘𝐾)‘𝑌))
30	15, 23, 27, 29	syl3anc 1369	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((lub‘𝐾)‘𝑋)(le‘𝐾)((lub‘𝐾)‘𝑌))
31		eqid 2738	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
32		eqid 2738	. . . . . . 7 ⊢ (oc‘𝐾) = (oc‘𝐾)
33	17, 28, 31, 32	omllaw4 37187	. . . . . 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 6760	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)))
36	2, 32, 3, 4, 5	polval2N 37847	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
37	11, 16, 36	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))
38		simprr 769	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))
39	37, 38	ineq12d 4144	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘𝑋) ∩ 𝑌) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
40		hlop 37303	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
41	11, 40	syl 17	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ OP)
42	17, 32	opoccl 37135	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
43	41, 21, 42	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾))
44	17, 31, 3, 4	pmapmeet 37714	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
45	11, 43, 25, 44	syl3anc 1369	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
46	39, 45	eqtr4d 2781	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘𝑋) ∩ 𝑌) = ((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))))
47	46	fveq2d 6760	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) = ( ⊥ ‘((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
48	11	hllatd 37305	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → 𝐾 ∈ Lat)
49	17, 31	latmcl 18073	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾) ∧ ((lub‘𝐾)‘𝑌) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾))
50	48, 43, 25, 49	syl3anc 1369	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾))
51	17, 32, 4, 5	polpmapN 37853	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾)) → ( ⊥ ‘((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) = ((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
52	11, 50, 51	syl2anc 583	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘((pmap‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) = ((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
53	47, 52	eqtrd 2778	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) = ((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))))
54	53, 38	ineq12d 4144	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = (((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
55	17, 32	opoccl 37135	. . . . . . 7 ⊢ ((𝐾 ∈ OP ∧ (((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) ∈ (Base‘𝐾))
56	41, 50, 55	syl2anc 583	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌))) ∈ (Base‘𝐾))
57	17, 31, 3, 4	pmapmeet 37714	. . . . . 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 1369	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))) = (((pmap‘𝐾)‘((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))) ∩ ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))))
59	54, 58	eqtr4d 2781	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ((pmap‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘((lub‘𝐾)‘𝑋))(meet‘𝐾)((lub‘𝐾)‘𝑌)))(meet‘𝐾)((lub‘𝐾)‘𝑌))))
60	2, 3, 4, 5	2polvalN 37855	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)))
61	11, 16, 60	syl2anc 583	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → ( ⊥ ‘( ⊥ ‘𝑋)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)))
62	35, 59, 61	3eqtr4d 2788	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌)))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))
63	62	ex 412	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ 𝑌 = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑌))) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))))
64	10, 63	sylan2d 604	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∩ cin 3882 ⊆ wss 3883 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 Basecbs 16840 lecple 16895 occoc 16896 lubclub 17942 meetcmee 17945 Latclat 18064 CLatccla 18131 OPcops 37113 OMLcoml 37116 Atomscatm 37204 HLchlt 37291 pmapcpmap 37438 ⊥_𝑃cpolN 37843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-riotaBAD 36894

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-undef 8060 df-proset 17928 df-poset 17946 df-plt 17963 df-lub 17979 df-glb 17980 df-join 17981 df-meet 17982 df-p0 18058 df-p1 18059 df-lat 18065 df-clat 18132 df-oposet 37117 df-ol 37119 df-oml 37120 df-covers 37207 df-ats 37208 df-atl 37239 df-cvlat 37263 df-hlat 37292 df-pmap 37445 df-polarityN 37844

This theorem is referenced by: poml5N 37895 poml6N 37896 pexmidlem6N 37916

W3C validator