Theorem trnsetN 41127

Description: The set of translations for a fiducial atom 𝐷. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)

Hypotheses

Ref	Expression
trnset.a	⊢ 𝐴 = (Atoms‘𝐾)
trnset.s	⊢ 𝑆 = (PSubSp‘𝐾)
trnset.p	⊢ + = (+𝑃‘𝐾)
trnset.o	⊢ ⊥ = (⊥𝑃‘𝐾)
trnset.w	⊢ 𝑊 = (WAtoms‘𝐾)
trnset.m	⊢ 𝑀 = (PAut‘𝐾)
trnset.l	⊢ 𝐿 = (Dil‘𝐾)
trnset.t	⊢ 𝑇 = (Trn‘𝐾)

Assertion

Ref	Expression
trnsetN	⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑇‘𝐷) = {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))})

Distinct variable groups:   𝑓,𝑞,𝑟,𝐾   𝑓,𝐿   𝑊,𝑞,𝑟   𝐷,𝑓,𝑞,𝑟

Allowed substitution hints:   𝐴(𝑓, 𝑟, 𝑞)   𝐵(𝑓, 𝑟, 𝑞)   + (𝑓, 𝑟, 𝑞)   𝑆(𝑓, 𝑟, 𝑞)   𝑇(𝑓, 𝑟, 𝑞)   𝐿(𝑟, 𝑞)   𝑀(𝑓, 𝑟, 𝑞)   ⊥ (𝑓, 𝑟, 𝑞)   𝑊(𝑓)

Proof of Theorem trnsetN

Dummy variable 𝑑 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		trnset.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
2		trnset.s	. . . 4 ⊢ 𝑆 = (PSubSp‘𝐾)
3		trnset.p	. . . 4 ⊢ + = (+𝑃‘𝐾)
4		trnset.o	. . . 4 ⊢ ⊥ = (⊥𝑃‘𝐾)
5		trnset.w	. . . 4 ⊢ 𝑊 = (WAtoms‘𝐾)
6		trnset.m	. . . 4 ⊢ 𝑀 = (PAut‘𝐾)
7		trnset.l	. . . 4 ⊢ 𝐿 = (Dil‘𝐾)
8		trnset.t	. . . 4 ⊢ 𝑇 = (Trn‘𝐾)
9	1, 2, 3, 4, 5, 6, 7, 8	trnfsetN 41126	. . 3 ⊢ (𝐾 ∈ 𝐵 → 𝑇 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))}))
10	9	fveq1d 6876	. 2 ⊢ (𝐾 ∈ 𝐵 → (𝑇‘𝐷) = ((𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})‘𝐷))
11		fveq2 6874	. . . 4 ⊢ (𝑑 = 𝐷 → (𝐿‘𝑑) = (𝐿‘𝐷))
12		fveq2 6874	. . . . 5 ⊢ (𝑑 = 𝐷 → (𝑊‘𝑑) = (𝑊‘𝐷))
13		sneq 4594	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → {𝑑} = {𝐷})
14	13	fveq2d 6878	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ( ⊥ ‘{𝑑}) = ( ⊥ ‘{𝐷}))
15	14	ineq2d 4166	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})))
16	14	ineq2d 4166	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷})))
17	15, 16	eqeq12d 2776	. . . . . 6 ⊢ (𝑑 = 𝐷 → (((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})) ↔ ((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))))
18	12, 17	raleqbidv 3334	. . . . 5 ⊢ (𝑑 = 𝐷 → (∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})) ↔ ∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))))
19	12, 18	raleqbidv 3334	. . . 4 ⊢ (𝑑 = 𝐷 → (∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})) ↔ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))))
20	11, 19	rabeqbidv 3429	. . 3 ⊢ (𝑑 = 𝐷 → {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))} = {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))})
21		eqid 2760	. . 3 ⊢ (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))}) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})
22		fvex 6887	. . . 4 ⊢ (𝐿‘𝐷) ∈ V
23	22	rabex 5300	. . 3 ⊢ {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))} ∈ V
24	20, 21, 23	fvmpt 6982	. 2 ⊢ (𝐷 ∈ 𝐴 → ((𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})‘𝐷) = {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))})
25	10, 24	sylan9eq 2815	1 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑇‘𝐷) = {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412   ∩ cin 3898  {csn 4584   ↦ cmpt 5186  ‘cfv 6528  (class class class)co 7409  Atomscatm 40234  PSubSpcpsubsp 40467  +_𝑃cpadd 40766  ⊥_𝑃cpolN 40873  WAtomscwpointsN 40957  PAutcpautN 40958  DilcdilN 41073  TrnctrnN 41074

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 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-trnN 41078

This theorem is used by:  istrnN  41128