Metamath Proof Explorer

Theorem trnsetN

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

Ref Expression
Hypotheses trnset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trnset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
trnset.p ⊢ + = ( +𝑃 ‘ 𝐾 )
trnset.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
trnset.w ⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
trnset.m ⊢ 𝑀 = ( PAut ‘ 𝐾 )
trnset.l ⊢ 𝐿 = ( Dil ‘ 𝐾 )
trnset.t ⊢ 𝑇 = ( Trn ‘ 𝐾 )
Assertion trnsetN ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑇 ‘ 𝐷 ) = { 𝑓 ∈ ( 𝐿 ‘ 𝐷 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) } )

Proof

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