Theorem pmapglb2N

Description: The projective map of the GLB of a set of lattice elements S . Variant of Theorem 15.5.2 of MaedaMaeda p. 62. Allows S = (/) . (Contributed by NM, 21-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapglb2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapglb2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	pmapglb2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmapglb2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	pmapglb2N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmapglb2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapglb2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
3		pmapglb2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		pmapglb2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
5		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
6		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
7	2 6	glb0N	⊢ ( 𝐾 ∈ OP → ( 𝐺 ‘ ∅ ) = ( 1. ‘ 𝐾 ) )
8	7	fveq2d	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = ( 𝑀 ‘ ( 1. ‘ 𝐾 ) ) )
9	6 3 4	pmap1N	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 1. ‘ 𝐾 ) ) = 𝐴 )
10	8 9	eqtrd	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 )
11	5 10	syl	⊢ ( 𝐾 ∈ HL → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 )
12		2fveq3	⊢ ( 𝑆 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) )
13		riin0	⊢ ( 𝑆 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) = 𝐴 )
14	12 13	eqeq12d	⊢ ( 𝑆 = ∅ → ( ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 ) )
15	11 14	syl5ibrcom	⊢ ( 𝐾 ∈ HL → ( 𝑆 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ) )
16	15	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ) )
17	1 2 4	pmapglb	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
18		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
19		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ HL )
20		ssel2	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
21	20	adantll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
22	1 3 4	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
23	19 21 22	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
24	18 23	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) )
25	24	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) ) )
26	25	eximdv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( ∃ 𝑥 𝑥 ∈ 𝑆 → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) ) )
27		n0	⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
28		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) )
29	26 27 28	3imtr4g	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 ≠ ∅ → ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) )
30	29	3impia	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
31		iinss	⊢ ( ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 → ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
32	30 31	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
33		sseqin2	⊢ ( ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
34	32 33	sylib	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
35	17 34	eqtr4d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) )
36	35	3expia	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 ≠ ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ) )
37	16 36	pm2.61dne	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) )