Theorem istrnN 40991

Description: The predicate "is a translation". (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
istrnN	⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝑇‘𝐷) ↔ (𝐹 ∈ (𝐿‘𝐷) ∧ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷})))))

Distinct variable groups:   𝑟,𝑞,𝐾   𝑊,𝑞,𝑟   𝐷,𝑞,𝑟   𝐹,𝑞,𝑟

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

Proof of Theorem istrnN

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	trnsetN 40990	. . 3 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑇‘𝐷) = {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))})
10	9	eleq2d 2851	. 2 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝑇‘𝐷) ↔ 𝐹 ∈ {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))}))
11		fveq1 6884	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑞) = (𝐹‘𝑞))
12	11	oveq2d 7435	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑞 + (𝑓‘𝑞)) = (𝑞 + (𝐹‘𝑞)))
13	12	ineq1d 4172	. . . . 5 ⊢ (𝑓 = 𝐹 → ((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})))
14		fveq1 6884	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑟) = (𝐹‘𝑟))
15	14	oveq2d 7435	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑟 + (𝑓‘𝑟)) = (𝑟 + (𝐹‘𝑟)))
16	15	ineq1d 4172	. . . . 5 ⊢ (𝑓 = 𝐹 → ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷})))
17	13, 16	eqeq12d 2781	. . . 4 ⊢ (𝑓 = 𝐹 → (((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷})) ↔ ((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷}))))
18	17	2ralbidv 3231	. . 3 ⊢ (𝑓 = 𝐹 → (∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷})) ↔ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷}))))
19	18	elrab 3652	. 2 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))} ↔ (𝐹 ∈ (𝐿‘𝐷) ∧ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷}))))
20	10, 19	bitrdi 290	1 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝑇‘𝐷) ↔ (𝐹 ∈ (𝐿‘𝐷) ∧ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷})))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  {crab 3418   ∩ cin 3905  {csn 4591  ‘cfv 6540  (class class class)co 7419  Atomscatm 40097  PSubSpcpsubsp 40330  +_𝑃cpadd 40629  ⊥_𝑃cpolN 40736  WAtomscwpointsN 40820  PAutcpautN 40821  DilcdilN 40936  TrnctrnN 40937

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-trnN 40941

This theorem is used by: (None)