dihmeetlem19N - Mathbox for Norm Megill

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

Theorem dihmeetlem19N 42127

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

**Hypotheses**
Ref	Expression
dihmeetlem14.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem14.l	⊢ ≤ = (le‘𝐾)
dihmeetlem14.h	⊢ 𝐻 = (LHyp‘𝐾)
dihmeetlem14.j	⊢ ∨ = (join‘𝐾)
dihmeetlem14.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem14.a	⊢ 𝐴 = (Atoms‘𝐾)
dihmeetlem14.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihmeetlem14.s	⊢ ⊕ = (LSSum‘𝑈)
dihmeetlem14.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
dihmeetlem19N	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

**Proof of Theorem dihmeetlem19N**
Step	Hyp	Ref	Expression
1		incom 4161	. . . 4 ⊢ ((𝐼‘𝑝) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑌) ∩ (𝐼‘𝑝))
2		dihmeetlem14.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
3		dihmeetlem14.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
4		dihmeetlem14.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
5		dihmeetlem14.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
6		dihmeetlem14.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
7		dihmeetlem14.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
8		dihmeetlem14.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
9		dihmeetlem14.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝑈)
10		dihmeetlem14.i	. . . . 5 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
11		eqid 2762	. . . . 5 ⊢ (0_g‘𝑈) = (0_g‘𝑈)
12	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	dihmeetlem18N 42126	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → ((𝐼‘𝑌) ∩ (𝐼‘𝑝)) = {(0_g‘𝑈)})
13	1, 12	eqtrid 2809	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → ((𝐼‘𝑝) ∩ (𝐼‘𝑌)) = {(0_g‘𝑈)})
14	13	oveq2d 7428	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))) = ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ {(0_g‘𝑈)}))
15		simpl1 1209	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
16		simpl2l 1244	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → 𝑋 ∈ 𝐵)
17		simpl3 1211	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → 𝑌 ∈ 𝐵)
18		simpr1 1212	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊))
19		simpr31 1281	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → 𝑝 ≤ 𝑋)
20		simpr33 1283	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝑋 ∧ 𝑌) ≤ 𝑊)
21	2, 3, 4, 5, 6, 7, 8, 9, 10	dihmeetlem12N 42120	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
22	15, 16, 17, 18, 19, 20, 21	syl33anc 1411	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
23	4, 8, 15	dvhlmod 41912	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → 𝑈 ∈ LMod)
24		simpl1l 1242	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → 𝐾 ∈ HL)
25	24	hllatd 40166	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → 𝐾 ∈ Lat)
26	2, 6	latmcl 18502	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
27	25, 16, 17, 26	syl3anc 1397	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝑋 ∧ 𝑌) ∈ 𝐵)
28		eqid 2762	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
29	2, 4, 10, 8, 28	dihlss 42052	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∧ 𝑌) ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (LSubSp‘𝑈))
30	15, 27, 29	syl2anc 595	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (LSubSp‘𝑈))
31	28	lsssubg 21089	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ (𝐼‘(𝑋 ∧ 𝑌)) ∈ (LSubSp‘𝑈)) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (SubGrp‘𝑈))
32	23, 30, 31	syl2anc 595	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (SubGrp‘𝑈))
33	11, 9	lsm01 19747	. . 3 ⊢ ((𝐼‘(𝑋 ∧ 𝑌)) ∈ (SubGrp‘𝑈) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ {(0_g‘𝑈)}) = (𝐼‘(𝑋 ∧ 𝑌)))
34	32, 33	syl 18	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ {(0_g‘𝑈)}) = (𝐼‘(𝑋 ∧ 𝑌)))
35	14, 22, 34	3eqtr3rd 2806	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ∩ cin 3903 {csn 4588 class class class wbr 5108 ‘cfv 6536 (class class class)co 7412 Basecbs 17275 lecple 17323 0_gc0g 17498 joincjn 18373 meetcmee 18374 Latclat 18493 SubGrpcsubg 19192 LSSumclsm 19710 LModclmod 20992 LSubSpclss 21063 Atomscatm 40065 HLchlt 40152 LHypclh 40786 DVecHcdvh 41880 DIsoHcdih 42030

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-riotaBAD 39755

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-tpos 8220 df-undef 8267 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-er 8692 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-n0 12511 df-z 12598 df-uz 12869 df-fz 13542 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-sca 17332 df-vsca 17333 df-0g 17500 df-mre 17644 df-mrc 17645 df-acs 17647 df-proset 18356 df-poset 18375 df-plt 18390 df-lub 18406 df-glb 18407 df-join 18408 df-meet 18409 df-p0 18485 df-p1 18486 df-lat 18494 df-clat 18561 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-grp 19009 df-minusg 19010 df-sbg 19011 df-subg 19195 df-cntz 19393 df-lsm 19712 df-cmn 19858 df-abl 19859 df-mgp 20223 df-rng 20237 df-ur 20270 df-ring 20323 df-oppr 20426 df-dvdsr 20446 df-unit 20447 df-invr 20477 df-dvr 20490 df-drng 20840 df-lmod 20994 df-lss 21064 df-lsp 21104 df-lvec 21235 df-oposet 39978 df-ol 39980 df-oml 39981 df-covers 40068 df-ats 40069 df-atl 40100 df-cvlat 40124 df-hlat 40153 df-llines 40300 df-lplanes 40301 df-lvols 40302 df-lines 40303 df-psubsp 40305 df-pmap 40306 df-padd 40598 df-lhyp 40790 df-laut 40791 df-ldil 40906 df-ltrn 40907 df-trl 40961 df-tendo 41557 df-edring 41559 df-disoa 41831 df-dvech 41881 df-dib 41941 df-dic 41975 df-dih 42031

This theorem is used by: dihmeetlem20N 42128

W3C validator