Theorem trlval2 40157

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 39356	. . 3 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	anim1i 615	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻))
3		eqid 2729	. . . . 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 40156	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = (℩𝑥 ∈ (Base‘𝐾)∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
12	11	3adant3 1132	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = (℩𝑥 ∈ (Base‘𝐾)∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
13		simp1l 1198	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
14		simp3l 1202	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
15	3, 7	atbase 39282	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
16	14, 15	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
17	3, 8, 9	ltrncl 40119	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐹‘𝑃) ∈ (Base‘𝐾))
18	16, 17	syld3an3 1411	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ (Base‘𝐾))
19	3, 5	latjcl 18398	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹‘𝑃) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
20	13, 16, 18, 19	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
21		simp1r 1199	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
22	3, 8	lhpbase 39992	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
23	21, 22	syl 17	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
24	3, 6	latmcl 18399	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾))
25	13, 20, 23, 24	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾))
26		simpl3l 1229	. . . . . 6 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝑃 ∈ 𝐴)
27		simpl3r 1230	. . . . . 6 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → ¬ 𝑃 ≤ 𝑊)
28		breq1 5110	. . . . . . . . . 10 ⊢ (𝑞 = 𝑃 → (𝑞 ≤ 𝑊 ↔ 𝑃 ≤ 𝑊))
29	28	notbid 318	. . . . . . . . 9 ⊢ (𝑞 = 𝑃 → (¬ 𝑞 ≤ 𝑊 ↔ ¬ 𝑃 ≤ 𝑊))
30		id 22	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑃 → 𝑞 = 𝑃)
31		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑃 → (𝐹‘𝑞) = (𝐹‘𝑃))
32	30, 31	oveq12d 7405	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑃 → (𝑞 ∨ (𝐹‘𝑞)) = (𝑃 ∨ (𝐹‘𝑃)))
33	32	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝑞 = 𝑃 → ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
34	33	eqeq2d 2740	. . . . . . . . 9 ⊢ (𝑞 = 𝑃 → (𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) ↔ 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
35	29, 34	imbi12d 344	. . . . . . . 8 ⊢ (𝑞 = 𝑃 → ((¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) ↔ (¬ 𝑃 ≤ 𝑊 → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))))
36	35	rspcv 3584	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) → (¬ 𝑃 ≤ 𝑊 → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))))
37	36	com23 86	. . . . . 6 ⊢ (𝑃 ∈ 𝐴 → (¬ 𝑃 ≤ 𝑊 → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))))
38	26, 27, 37	sylc 65	. . . . 5 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) → 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
39		simp11 1204	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → (𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻))
40		simp12 1205	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → 𝐹 ∈ 𝑇)
41		simp13l 1289	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → 𝑃 ∈ 𝐴)
42		simp13r 1290	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑃 ≤ 𝑊)
43		simp3 1138	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
44		simp2 1137	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ≤ 𝑊)
45	4, 5, 6, 7, 8, 9	ltrnu 40115	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))
46	39, 40, 41, 42, 43, 44, 45	syl222anc 1388	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))
47		eqeq2 2741	. . . . . . . . . . 11 ⊢ (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ↔ 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))
48	47	biimpd 229	. . . . . . . . . 10 ⊢ (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))
49	46, 48	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))
50	49	3exp 1119	. . . . . . . 8 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (¬ 𝑞 ≤ 𝑊 → (𝑞 ∈ 𝐴 → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))))
51	50	com24 95	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → (𝑞 ∈ 𝐴 → (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))))
52	51	ralrimdv 3131	. . . . . 6 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → ∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
53	52	adantr 480	. . . . 5 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) → ∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))))
54	38, 53	impbid 212	. . . 4 ⊢ ((((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)) ↔ 𝑥 = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
55	25, 54	riota5 7373	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (℩𝑥 ∈ (Base‘𝐾)∀𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 → 𝑥 = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊))) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
56	12, 55	eqtrd 2764	. 2 ⊢ (((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
57	2, 56	syl3an1 1163	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044   class class class wbr 5107  ‘cfv 6511  ℩crio 7343  (class class class)co 7387  Basecbs 17179  lecple 17227  joincjn 18272  meetcmee 18273  Latclat 18390  Atomscatm 39256  HLchlt 39343  LHypclh 39978  LTrncltrn 40095  trLctrl 40152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-map 8801  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-lat 18391  df-ats 39260  df-atl 39291  df-cvlat 39315  df-hlat 39344  df-lhyp 39982  df-laut 39983  df-ldil 40098  df-ltrn 40099  df-trl 40153

This theorem is referenced by:  trlcl  40158  trlcnv  40159  trljat1  40160  trljat2  40161  trlat  40163  trl0  40164  trlle  40178  trlval3  40181  trlval5  40183  cdlemd6  40197  cdlemf  40557  cdlemg4a  40602  cdlemg4b1  40603  cdlemg4b2  40604  cdlemg4  40611  cdlemg11b  40636  cdlemg13a  40645  cdlemg13  40646  cdlemg17a  40655  cdlemg17dN  40657  cdlemg17e  40659  cdlemg17f  40660  trlcoabs2N  40716  trlcolem  40720  cdlemg42  40723  cdlemg43  40724  cdlemi1  40812  cdlemk4  40828  cdlemk39  40910  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  cdlemm10N  41112  cdlemn2  41189  cdlemn10  41200  dihjatcclem3  41414