Theorem trlval 39028

Description: The value of the trace of a lattice translation. (Contributed by NM, 20-May-2012.)

Hypotheses

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

Assertion

Ref	Expression
trlval	⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))

Distinct variable groups:   𝐴,𝑝   𝑥,𝐵   𝑥,𝑝,𝐾   𝑊,𝑝,𝑥   𝐹,𝑝,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑝)   𝑅(𝑥,𝑝)   𝑇(𝑥,𝑝)   𝐻(𝑥,𝑝)   ∨ (𝑥,𝑝)   ≤ (𝑥,𝑝)   ∧ (𝑥,𝑝)   𝑉(𝑥,𝑝)

Proof of Theorem trlval

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		trlset.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
2		trlset.l	. . . 4 ⊢ ≤ = (le‘𝐾)
3		trlset.j	. . . 4 ⊢ ∨ = (join‘𝐾)
4		trlset.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
5		trlset.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
6		trlset.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
7		trlset.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
8		trlset.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	trlset 39027	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝑅 = (𝑓 ∈ 𝑇 ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊)))))
10	9	fveq1d 6893	. 2 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝑅‘𝐹) = ((𝑓 ∈ 𝑇 ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊))))‘𝐹))
11		fveq1 6890	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑝) = (𝐹‘𝑝))
12	11	oveq2d 7424	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑝 ∨ (𝑓‘𝑝)) = (𝑝 ∨ (𝐹‘𝑝)))
13	12	oveq1d 7423	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))
14	13	eqeq2d 2743	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) ↔ 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊)))
15	14	imbi2d 340	. . . . 5 ⊢ (𝑓 = 𝐹 → ((¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊)) ↔ (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))
16	15	ralbidv 3177	. . . 4 ⊢ (𝑓 = 𝐹 → (∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊)) ↔ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))
17	16	riotabidv 7366	. . 3 ⊢ (𝑓 = 𝐹 → (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊))) = (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))
18		eqid 2732	. . 3 ⊢ (𝑓 ∈ 𝑇 ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊)))) = (𝑓 ∈ 𝑇 ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊))))
19		riotaex 7368	. . 3 ⊢ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))) ∈ V
20	17, 18, 19	fvmpt 6998	. 2 ⊢ (𝐹 ∈ 𝑇 → ((𝑓 ∈ 𝑇 ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊))))‘𝐹) = (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))
21	10, 20	sylan9eq 2792	1 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061   class class class wbr 5148   ↦ cmpt 5231  ‘cfv 6543  ℩crio 7363  (class class class)co 7408  Basecbs 17143  lecple 17203  joincjn 18263  meetcmee 18264  Atomscatm 38128  LHypclh 38850  LTrncltrn 38967  trLctrl 39024

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-trl 39025

This theorem is referenced by:  trlval2  39029