Theorem trlval2 41188

Description: The value of the trace of a lattice translation, given any atom 𝑃 not under the fiducial co-atom 𝑊. Note: this requires only the weaker assumption 𝐾 ∈ Lat; we use 𝐾 ∈ HL for convenience. (Contributed by NM, 20-May-2012.)

Hypotheses

Ref	Expression
trlval2.l	⊢ ≤ = (le‘𝐾)
trlval2.j	⊢ ∨ = (join‘𝐾)
trlval2.m	⊢ ∧ = (meet‘𝐾)
trlval2.a	⊢ 𝐴 = (Atoms‘𝐾)
trlval2.h	⊢ 𝐻 = (LHyp‘𝐾)
trlval2.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlval2.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

Assertion

Ref	Expression
trlval2	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))

Proof of Theorem trlval2

Dummy variables 𝑥 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hllat 40388	. . 3 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	anim1i 627	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻))
3		eqid 2761	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
4		trlval2.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
5		trlval2.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
6		trlval2.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
7		trlval2.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
8		trlval2.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
9		trlval2.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
10		trlval2.r	. . . . 5 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
11	3, 4, 5, 6, 7, 8, 9, 10	trlval 41187	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = (℩𝑥 ∈ (Base‘𝐾)∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
12	11	3adant3 1150	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = (℩𝑥 ∈ (Base‘𝐾)∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
13		simp1l 1216	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
14		simp3l 1220	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
15	3, 7	atbase 40314	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
16	14, 15	syl 18	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
17	3, 8, 9	ltrncl 41150	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐹‘𝑃) ∈ (Base‘𝐾))
18	16, 17	syld3an3 1436	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ (Base‘𝐾))
19	3, 5	latjcl 18593	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹‘𝑃) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
20	13, 16, 18, 19	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
21		simp1r 1217	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
22	3, 8	lhpbase 41023	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
23	21, 22	syl 18	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
24	3, 6	latmcl 18594	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾))
25	13, 20, 23, 24	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾))
26		simpl3l 1247	. . . . . 6 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝑃 ∈ 𝐴)
27		simpl3r 1248	. . . . . 6 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → ¬ 𝑃 ≤ 𝑊)
28		breq1 5106	. . . . . . . . . 10 ⊢ (𝑞 = 𝑃 → (𝑞 ≤ 𝑊 ↔ 𝑃 ≤ 𝑊))
29	28	notbid 321	. . . . . . . . 9 ⊢ (𝑞 = 𝑃 → (¬ 𝑞 ≤ 𝑊 ↔ ¬ 𝑃 ≤ 𝑊))
30		id 23	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑃 → 𝑞 = 𝑃)
31		fveq2 6877	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑃 → (𝐹‘𝑞) = (𝐹‘𝑃))
32	30, 31	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑃 → (𝑞 ∨ (𝐹‘𝑞)) = (𝑃 ∨ (𝐹‘𝑃)))
33	32	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝑞 = 𝑃 → ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
34	33	eqeq2d 2772	. . . . . . . . 9 ⊢ (𝑞 = 𝑃 → (𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) ↔ 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
35	29, 34	imbi12d 347	. . . . . . . 8 ⊢ (𝑞 = 𝑃 → ((¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) ↔ (¬ 𝑃 ≤ 𝑊 → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))))
36	35	rspcv 3573	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) → (¬ 𝑃 ≤ 𝑊 → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))))
37	36	com23 87	. . . . . 6 ⊢ (𝑃 ∈ 𝐴 → (¬ 𝑃 ≤ 𝑊 → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))))
38	26, 27, 37	sylc 66	. . . . 5 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
39		simp11 1222	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → (𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻))
40		simp12 1223	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → 𝐹 ∈ 𝑇)
41		simp13l 1307	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → 𝑃 ∈ 𝐴)
42		simp13r 1308	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑃 ≤ 𝑊)
43		simp3 1156	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
44		simp2 1155	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ≤ 𝑊)
45	4, 5, 6, 7, 8, 9	ltrnu 41146	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))
46	39, 40, 41, 42, 43, 44, 45	syl222anc 1413	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))
47		eqeq2 2773	. . . . . . . . . . 11 ⊢ (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ↔ 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))
48	47	biimpd 232	. . . . . . . . . 10 ⊢ (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))
49	46, 48	syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))
50	49	3exp 1137	. . . . . . . 8 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (¬ 𝑞 ≤ 𝑊 → (𝑞 ∈ 𝐴 → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))))
51	50	com24 96	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → (𝑞 ∈ 𝐴 → (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))))
52	51	ralrimdv 3161	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → ∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
53	52	adantr 486	. . . . 5 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → ∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
54	38, 53	impbid 215	. . . 4 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) ↔ 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
55	25, 54	riota5 7398	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (℩𝑥 ∈ (Base‘𝐾)∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
56	12, 55	eqtrd 2796	. 2 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
57	2, 56	syl3an1 1181	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077   class class class wbr 5103  ‘cfv 6531  ℩crio 7368  (class class class)co 7412  Basecbs 17367  lecple 17415  joincjn 18465  meetcmee 18466  Latclat 18585  Atomscatm 40288  HLchlt 40375  LHypclh 41009  LTrncltrn 41126  trLctrl 41183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8833  df-lub 18498  df-glb 18499  df-join 18500  df-meet 18501  df-lat 18586  df-ats 40292  df-atl 40323  df-cvlat 40347  df-hlat 40376  df-lhyp 41013  df-laut 41014  df-ldil 41129  df-ltrn 41130  df-trl 41184

This theorem is used by:  trlcl  41189  trlcnv  41190  trljat1  41191  trljat2  41192  trlat  41194  trl0  41195  trlle  41209  trlval3  41212  trlval5  41214  cdlemd6  41228  cdlemf  41588  cdlemg4a  41633  cdlemg4b1  41634  cdlemg4b2  41635  cdlemg4  41642  cdlemg11b  41667  cdlemg13a  41676  cdlemg13  41677  cdlemg17a  41686  cdlemg17dN  41688  cdlemg17e  41690  cdlemg17f  41691  trlcoabs2N  41747  trlcolem  41751  cdlemg42  41754  cdlemg43  41755  cdlemi1  41843  cdlemk4  41859  cdlemk39  41941  dia2dimlem1  42089  dia2dimlem2  42090  dia2dimlem3  42091  cdlemm10N  42143  cdlemn2  42220  cdlemn10  42231  dihjatcclem3  42445