This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istrnN

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

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 trnsetN ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑇 ‘ 𝐷 ) = { 𝑓 ∈ ( 𝐿 ‘ 𝐷 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) } )
10 9 eleq2d ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐹 ∈ ( 𝑇 ‘ 𝐷 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐿 ‘ 𝐷 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) } ) )
11 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑞 ) )
12 11 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) = ( 𝑞 + ( 𝐹 ‘ 𝑞 ) ) )
13 12 ineq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑞 + ( 𝐹 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) )
14 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑟 ) )
15 14 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) = ( 𝑟 + ( 𝐹 ‘ 𝑟 ) ) )
16 15 ineq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝐹 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) )
17 13 16 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) ↔ ( ( 𝑞 + ( 𝐹 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝐹 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) ) )
18 17 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) ↔ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝐹 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝐹 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) ) )
19 18 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐿 ‘ 𝐷 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) } ↔ ( 𝐹 ∈ ( 𝐿 ‘ 𝐷 ) ∧ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝐹 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝐹 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) ) )
20 10 19 bitrdi ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐹 ∈ ( 𝑇 ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝐿 ‘ 𝐷 ) ∧ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝐷 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝐷 ) ( ( 𝑞 + ( 𝐹 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝐹 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝐷 } ) ) ) ) )