Theorem dihmeetlem4preN 41774

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dihmeetlem4.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem4.l	⊢ ≤ = (le‘𝐾)
dihmeetlem4.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem4.a	⊢ 𝐴 = (Atoms‘𝐾)
dihmeetlem4.h	⊢ 𝐻 = (LHyp‘𝐾)
dihmeetlem4.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihmeetlem4.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihmeetlem4.z	⊢ 0 = (0g‘𝑈)
dihmeetlem4.g	⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
dihmeetlem4.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
dihmeetlem4.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dihmeetlem4.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
dihmeetlem4.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
dihmeetlem4.o	⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))

Assertion

Ref	Expression
dihmeetlem4preN	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 })

Distinct variable groups:   ≤ ,𝑔   𝐴,𝑔   𝑔,ℎ,𝐻   𝐵,ℎ   𝑔,𝐾,ℎ   𝑄,𝑔   𝑇,𝑔,ℎ   𝑔,𝑊,ℎ   𝑃,𝑔

Allowed substitution hints:   𝐴(ℎ)   𝐵(𝑔)   𝑃(ℎ)   𝑄(ℎ)   𝑅(𝑔,ℎ)   𝑈(𝑔,ℎ)   𝐸(𝑔,ℎ)   𝐺(𝑔,ℎ)   𝐼(𝑔,ℎ)   ≤ (ℎ)   ∧ (𝑔,ℎ)   𝑂(𝑔,ℎ)   𝑋(𝑔,ℎ)   0 (𝑔,ℎ)

Proof of Theorem dihmeetlem4preN

Dummy variables 𝑓 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dihmeetlem4.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
2		dihmeetlem4.i	. . . . 5 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
3	1, 2	dihvalrel 41747	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑄))
4		relin1 5765	. . . 4 ⊢ (Rel (𝐼‘𝑄) → Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))))
5	3, 4	syl 17	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))))
6	5	3ad2ant1 1134	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))))
7	1, 2	dihvalrel 41747	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(0.‘𝐾)))
8		eqid 2737	. . . . . 6 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		dihmeetlem4.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
10		dihmeetlem4.z	. . . . . 6 ⊢ 0 = (0g‘𝑈)
11	8, 1, 2, 9, 10	dih0 41748	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘(0.‘𝐾)) = { 0 })
12	11	releqd 5732	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Rel (𝐼‘(0.‘𝐾)) ↔ Rel { 0 }))
13	7, 12	mpbid 232	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel { 0 })
14	13	3ad2ant1 1134	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → Rel { 0 })
15		id 22	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
16		elin 3906	. . . 4 ⊢ (⟨𝑓, 𝑠⟩ ∈ ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) ↔ (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊))))
17		dihmeetlem4.l	. . . . . . . . . 10 ⊢ ≤ = (le‘𝐾)
18		dihmeetlem4.a	. . . . . . . . . 10 ⊢ 𝐴 = (Atoms‘𝐾)
19		dihmeetlem4.p	. . . . . . . . . 10 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
20		dihmeetlem4.t	. . . . . . . . . 10 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
21		dihmeetlem4.e	. . . . . . . . . 10 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
22		dihmeetlem4.g	. . . . . . . . . 10 ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
23		vex 3434	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
24		vex 3434	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
25	17, 18, 1, 19, 20, 21, 2, 22, 23, 24	dihopelvalcqat 41714	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ↔ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸)))
26	25	3adant2 1132	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ↔ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸)))
27		simp1 1137	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
28		simp1l 1199	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐾 ∈ HL)
29	28	hllatd 39832	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐾 ∈ Lat)
30		simp2l 1201	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑋 ∈ 𝐵)
31		simp1r 1200	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
32		dihmeetlem4.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐾)
33	32, 1	lhpbase 40466	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
34	31, 33	syl 17	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑊 ∈ 𝐵)
35		dihmeetlem4.m	. . . . . . . . . . 11 ⊢ ∧ = (meet‘𝐾)
36	32, 35	latmcl 18403	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
37	29, 30, 34, 36	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
38	32, 17, 35	latmle2 18428	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊)
39	29, 30, 34, 38	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑋 ∧ 𝑊) ≤ 𝑊)
40		dihmeetlem4.r	. . . . . . . . . 10 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
41		dihmeetlem4.o	. . . . . . . . . 10 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
42	32, 17, 1, 20, 40, 41, 2	dihopelvalbN 41706	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)))
43	27, 37, 39, 42	syl12anc 837	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)))
44	26, 43	anbi12d 633	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))))
45		simprll 779	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝑓 = (𝑠‘𝐺))
46		simprrr 782	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝑠 = 𝑂)
47	46	fveq1d 6840	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑠‘𝐺) = (𝑂‘𝐺))
48		simpl1 1193	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
49	17, 18, 1, 19	lhpocnel2 40487	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
50	48, 49	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
51		simpl3 1195	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
52	17, 18, 1, 20, 22	ltrniotacl 41047	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
53	48, 50, 51, 52	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝐺 ∈ 𝑇)
54	41, 32	tendo02 41255	. . . . . . . . . . 11 ⊢ (𝐺 ∈ 𝑇 → (𝑂‘𝐺) = ( I ↾ 𝐵))
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑂‘𝐺) = ( I ↾ 𝐵))
56	45, 47, 55	3eqtrd 2776	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝑓 = ( I ↾ 𝐵))
57	56, 46	jca 511	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂))
58		simpl1 1193	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
59	58, 49	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
60		simpl3 1195	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
61	58, 59, 60, 52	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝐺 ∈ 𝑇)
62	61, 54	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑂‘𝐺) = ( I ↾ 𝐵))
63		simprr 773	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑠 = 𝑂)
64	63	fveq1d 6840	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑠‘𝐺) = (𝑂‘𝐺))
65		simprl 771	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑓 = ( I ↾ 𝐵))
66	62, 64, 65	3eqtr4rd 2783	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑓 = (𝑠‘𝐺))
67	32, 1, 20, 21, 41	tendo0cl 41258	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸)
68	58, 67	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑂 ∈ 𝐸)
69	63, 68	eqeltrd 2837	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑠 ∈ 𝐸)
70	32, 1, 20	idltrn 40618	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇)
71	58, 70	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → ( I ↾ 𝐵) ∈ 𝑇)
72	65, 71	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑓 ∈ 𝑇)
73	65	fveq2d 6842	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘𝑓) = (𝑅‘( I ↾ 𝐵)))
74	32, 8, 1, 40	trlid0 40644	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾))
75	58, 74	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾))
76	73, 75	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘𝑓) = (0.‘𝐾))
77		simpl1l 1226	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝐾 ∈ HL)
78		hlatl 39828	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
79	77, 78	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝐾 ∈ AtLat)
80	37	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
81	32, 17, 8	atl0le 39772	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ AtLat ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (0.‘𝐾) ≤ (𝑋 ∧ 𝑊))
82	79, 80, 81	syl2anc 585	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (0.‘𝐾) ≤ (𝑋 ∧ 𝑊))
83	76, 82	eqbrtrd 5108	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))
84	72, 83, 63	jca31 514	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))
85	66, 69, 84	jca31 514	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)))
86	57, 85	impbida 801	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)) ↔ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)))
87	44, 86	bitrd 279	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)))
88		opex 5415	. . . . . . . 8 ⊢ ⟨𝑓, 𝑠⟩ ∈ V
89	88	elsn 4583	. . . . . . 7 ⊢ (⟨𝑓, 𝑠⟩ ∈ {⟨( I ↾ 𝐵), 𝑂⟩} ↔ ⟨𝑓, 𝑠⟩ = ⟨( I ↾ 𝐵), 𝑂⟩)
90	23, 24	opth 5428	. . . . . . 7 ⊢ (⟨𝑓, 𝑠⟩ = ⟨( I ↾ 𝐵), 𝑂⟩ ↔ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂))
91	89, 90	bitr2i 276	. . . . . 6 ⊢ ((𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂) ↔ ⟨𝑓, 𝑠⟩ ∈ {⟨( I ↾ 𝐵), 𝑂⟩})
92	87, 91	bitrdi 287	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ ⟨𝑓, 𝑠⟩ ∈ {⟨( I ↾ 𝐵), 𝑂⟩}))
93	32, 1, 20, 9, 10, 41	dvh0g 41579	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 = ⟨( I ↾ 𝐵), 𝑂⟩)
94	93	3ad2ant1 1134	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 0 = ⟨( I ↾ 𝐵), 𝑂⟩)
95	94	sneqd 4580	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → { 0 } = {⟨( I ↾ 𝐵), 𝑂⟩})
96	95	eleq2d 2823	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ { 0 } ↔ ⟨𝑓, 𝑠⟩ ∈ {⟨( I ↾ 𝐵), 𝑂⟩}))
97	92, 96	bitr4d 282	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑄) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ ⟨𝑓, 𝑠⟩ ∈ { 0 }))
98	16, 97	bitrid 283	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) ↔ ⟨𝑓, 𝑠⟩ ∈ { 0 }))
99	98	eqrelrdv2 5748	. 2 ⊢ (((Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) ∧ Rel { 0 }) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 })
100	6, 14, 15, 99	syl21anc 838	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 })

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ∩ cin 3889  {csn 4568  ⟨cop 4574   class class class wbr 5086   ↦ cmpt 5167   I cid 5522   ↾ cres 5630  Rel wrel 5633  ‘cfv 6496  ℩crio 7320  (class class class)co 7364  Basecbs 17176  lecple 17224  occoc 17225  0_gc0g 17399  meetcmee 18275  0.cp0 18384  Latclat 18394  Atomscatm 39731  AtLatcal 39732  HLchlt 39818  LHypclh 40452  LTrncltrn 40569  trLctrl 40626  TEndoctendo 41220  DVecHcdvh 41546  DIsoHcdih 41696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112  ax-riotaBAD 39421

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-om 7815  df-1st 7939  df-2nd 7940  df-tpos 8173  df-undef 8220  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-er 8640  df-map 8772  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-nn 12172  df-2 12241  df-3 12242  df-4 12243  df-5 12244  df-6 12245  df-n0 12435  df-z 12522  df-uz 12786  df-fz 13459  df-struct 17114  df-sets 17131  df-slot 17149  df-ndx 17161  df-base 17177  df-ress 17198  df-plusg 17230  df-mulr 17231  df-sca 17233  df-vsca 17234  df-0g 17401  df-proset 18257  df-poset 18276  df-plt 18291  df-lub 18307  df-glb 18308  df-join 18309  df-meet 18310  df-p0 18386  df-p1 18387  df-lat 18395  df-clat 18462  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18749  df-grp 18909  df-minusg 18910  df-sbg 18911  df-subg 19096  df-cntz 19289  df-lsm 19608  df-cmn 19754  df-abl 19755  df-mgp 20119  df-rng 20131  df-ur 20160  df-ring 20213  df-oppr 20314  df-dvdsr 20334  df-unit 20335  df-invr 20365  df-dvr 20378  df-drng 20705  df-lmod 20854  df-lss 20924  df-lsp 20964  df-lvec 21096  df-oposet 39644  df-ol 39646  df-oml 39647  df-covers 39734  df-ats 39735  df-atl 39766  df-cvlat 39790  df-hlat 39819  df-llines 39966  df-lplanes 39967  df-lvols 39968  df-lines 39969  df-psubsp 39971  df-pmap 39972  df-padd 40264  df-lhyp 40456  df-laut 40457  df-ldil 40572  df-ltrn 40573  df-trl 40627  df-tendo 41223  df-edring 41225  df-disoa 41497  df-dvech 41547  df-dib 41607  df-dic 41641  df-dih 41697

This theorem is referenced by:  dihmeetlem4N  41775