Theorem dihglblem3N 40768

Description: Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dihglblem.b	⊢ 𝐵 = (Base‘𝐾)
dihglblem.l	⊢ ≤ = (le‘𝐾)
dihglblem.m	⊢ ∧ = (meet‘𝐾)
dihglblem.g	⊢ 𝐺 = (glb‘𝐾)
dihglblem.h	⊢ 𝐻 = (LHyp‘𝐾)
dihglblem.t	⊢ 𝑇 = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)}
dihglblem.i	⊢ 𝐽 = ((DIsoB‘𝐾)‘𝑊)
dihglblem.ih	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)

Assertion

Ref	Expression
dihglblem3N	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑇)) = ∩ 𝑥 ∈ 𝑇 (𝐼‘𝑥))

Distinct variable groups:   𝑥,𝑢,𝑣, ∧   𝑥, ≤   𝑥,𝐵,𝑢   𝑥,𝐺   𝑥,𝐻   𝑥,𝐾   𝑥,𝑆,𝑢,𝑣   𝑥,𝑇   𝑥,𝑊,𝑢,𝑣   𝑢, ≤ ,𝑣   𝑣,𝐵   𝑢,𝐺,𝑣   𝑢,𝐻,𝑣   𝑢,𝐾,𝑣

Allowed substitution hints:   𝑇(𝑣,𝑢)   𝐼(𝑥,𝑣,𝑢)   𝐽(𝑥,𝑣,𝑢)

Proof of Theorem dihglblem3N

Step	Hyp	Ref	Expression
1		simp1 1134	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		dihglblem.t	. . . . . 6 ⊢ 𝑇 = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)}
3		simp11l 1282	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝐾 ∈ HL)
4	3	hllatd 38836	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝐾 ∈ Lat)
5		simp12l 1284	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
6		simp3 1136	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ 𝑆)
7	5, 6	sseldd 3981	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ 𝐵)
8		simp11r 1283	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑊 ∈ 𝐻)
9		dihglblem.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐾)
10		dihglblem.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (LHyp‘𝐾)
11	9, 10	lhpbase 39471	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
12	8, 11	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑊 ∈ 𝐵)
13		dihglblem.l	. . . . . . . . . . . 12 ⊢ ≤ = (le‘𝐾)
14		dihglblem.m	. . . . . . . . . . . 12 ⊢ ∧ = (meet‘𝐾)
15	9, 13, 14	latmle2 18456	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑣 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑣 ∧ 𝑊) ≤ 𝑊)
16	4, 7, 12, 15	syl3anc 1369	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → (𝑣 ∧ 𝑊) ≤ 𝑊)
17	16	3expia 1119	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵) → (𝑣 ∈ 𝑆 → (𝑣 ∧ 𝑊) ≤ 𝑊))
18		breq1 5151	. . . . . . . . . 10 ⊢ (𝑢 = (𝑣 ∧ 𝑊) → (𝑢 ≤ 𝑊 ↔ (𝑣 ∧ 𝑊) ≤ 𝑊))
19	18	biimprcd 249	. . . . . . . . 9 ⊢ ((𝑣 ∧ 𝑊) ≤ 𝑊 → (𝑢 = (𝑣 ∧ 𝑊) → 𝑢 ≤ 𝑊))
20	17, 19	syl6 35	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵) → (𝑣 ∈ 𝑆 → (𝑢 = (𝑣 ∧ 𝑊) → 𝑢 ≤ 𝑊)))
21	20	rexlimdv 3150	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵) → (∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊) → 𝑢 ≤ 𝑊))
22	21	ss2rabdv 4071	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} ⊆ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊})
23	2, 22	eqsstrid 4028	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑇 ⊆ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊})
24		dihglblem.i	. . . . . . 7 ⊢ 𝐽 = ((DIsoB‘𝐾)‘𝑊)
25	9, 13, 10, 24	dibdmN 40630	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → dom 𝐽 = {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊})
26	25	3ad2ant1 1131	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → dom 𝐽 = {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊})
27	23, 26	sseqtrrd 4021	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑇 ⊆ dom 𝐽)
28		dihglblem.g	. . . . . 6 ⊢ 𝐺 = (glb‘𝐾)
29	9, 13, 14, 28, 10, 2	dihglblem2aN 40766	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → 𝑇 ≠ ∅)
30	29	3adant3 1130	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑇 ≠ ∅)
31	28, 10, 24	dibglbN 40639	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑇 ⊆ dom 𝐽 ∧ 𝑇 ≠ ∅)) → (𝐽‘(𝐺‘𝑇)) = ∩ 𝑥 ∈ 𝑇 (𝐽‘𝑥))
32	1, 27, 30, 31	syl12anc 836	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐽‘(𝐺‘𝑇)) = ∩ 𝑥 ∈ 𝑇 (𝐽‘𝑥))
33	9, 13, 14, 28, 10, 2	dihglblem2N 40767	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) = (𝐺‘𝑇))
34	33	3adant2r 1177	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) = (𝐺‘𝑇))
35	34	fveq2d 6901	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐽‘(𝐺‘𝑆)) = (𝐽‘(𝐺‘𝑇)))
36		simpl1 1189	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
37	23	sselda 3980	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊})
38		breq1 5151	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (𝑢 ≤ 𝑊 ↔ 𝑥 ≤ 𝑊))
39	38	elrab 3682	. . . . . 6 ⊢ (𝑥 ∈ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊} ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊))
40	37, 39	sylib 217	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊))
41		dihglblem.ih	. . . . . 6 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
42	9, 13, 10, 41, 24	dihvalb 40710	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊)) → (𝐼‘𝑥) = (𝐽‘𝑥))
43	36, 40, 42	syl2anc 583	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → (𝐼‘𝑥) = (𝐽‘𝑥))
44	43	iineq2dv 5021	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → ∩ 𝑥 ∈ 𝑇 (𝐼‘𝑥) = ∩ 𝑥 ∈ 𝑇 (𝐽‘𝑥))
45	32, 35, 44	3eqtr4rd 2779	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → ∩ 𝑥 ∈ 𝑇 (𝐼‘𝑥) = (𝐽‘(𝐺‘𝑆)))
46		simp1l 1195	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL)
47		hlclat 38830	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
48	46, 47	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat)
49		simp2l 1197	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵)
50	9, 28	clatglbcl 18496	. . . 4 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
51	48, 49, 50	syl2anc 583	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵)
52		simp3 1136	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊)
53	9, 13, 10, 41, 24	dihvalb 40710	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = (𝐽‘(𝐺‘𝑆)))
54	1, 51, 52, 53	syl12anc 836	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = (𝐽‘(𝐺‘𝑆)))
55	34	fveq2d 6901	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = (𝐼‘(𝐺‘𝑇)))
56	45, 54, 55	3eqtr2rd 2775	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑇)) = ∩ 𝑥 ∈ 𝑇 (𝐼‘𝑥))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   ≠ wne 2937  ∃wrex 3067  {crab 3429   ⊆ wss 3947  ∅c0 4323  ∩ ciin 4997   class class class wbr 5148  dom cdm 5678  ‘cfv 6548  (class class class)co 7420  Basecbs 17179  lecple 17239  glbcglb 18301  meetcmee 18303  Latclat 18422  CLatccla 18489  HLchlt 38822  LHypclh 39457  DIsoBcdib 40611  DIsoHcdih 40701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-map 8846  df-proset 18286  df-poset 18304  df-plt 18321  df-lub 18337  df-glb 18338  df-join 18339  df-meet 18340  df-p0 18416  df-p1 18417  df-lat 18423  df-clat 18490  df-oposet 38648  df-ol 38650  df-oml 38651  df-covers 38738  df-ats 38739  df-atl 38770  df-cvlat 38794  df-hlat 38823  df-lhyp 39461  df-laut 39462  df-ldil 39577  df-ltrn 39578  df-trl 39632  df-disoa 40502  df-dib 40612  df-dih 40702

This theorem is referenced by:  dihglblem3aN  40769

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »