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 ( ( 𝐾𝐵𝐷𝐴 ) → ( 𝐹 ∈ ( 𝑇𝐷 ) ↔ ( 𝐹 ∈ ( 𝐿𝐷 ) ∧ ∀ 𝑞 ∈ ( 𝑊𝐷 ) ∀ 𝑟 ∈ ( 𝑊𝐷 ) ( ( 𝑞 + ( 𝐹𝑞 ) ) ∩ ( ‘ { 𝐷 } ) ) = ( ( 𝑟 + ( 𝐹𝑟 ) ) ∩ ( ‘ { 𝐷 } ) ) ) ) )