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