Theorem trnfsetN

Description: The mapping from fiducial atom to set of translations. (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	trnfsetN	⊢ ( 𝐾 ∈ 𝐶 → 𝑇 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )

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		elex	⊢ ( 𝐾 ∈ 𝐶 → 𝐾 ∈ V )
10		fveq2	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
11	10 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
12		fveq2	⊢ ( 𝑘 = 𝐾 → ( Dil ‘ 𝑘 ) = ( Dil ‘ 𝐾 ) )
13	12 7	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Dil ‘ 𝑘 ) = 𝐿 )
14	13	fveq1d	⊢ ( 𝑘 = 𝐾 → ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) = ( 𝐿 ‘ 𝑑 ) )
15		fveq2	⊢ ( 𝑘 = 𝐾 → ( WAtoms ‘ 𝑘 ) = ( WAtoms ‘ 𝐾 ) )
16	15 5	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( WAtoms ‘ 𝑘 ) = 𝑊 )
17	16	fveq1d	⊢ ( 𝑘 = 𝐾 → ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) = ( 𝑊 ‘ 𝑑 ) )
18		fveq2	⊢ ( 𝑘 = 𝐾 → ( +𝑃 ‘ 𝑘 ) = ( +𝑃 ‘ 𝐾 ) )
19	18 3	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( +𝑃 ‘ 𝑘 ) = + )
20	19	oveqd	⊢ ( 𝑘 = 𝐾 → ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) = ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) )
21		fveq2	⊢ ( 𝑘 = 𝐾 → ( ⊥𝑃 ‘ 𝑘 ) = ( ⊥𝑃 ‘ 𝐾 ) )
22	21 4	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( ⊥𝑃 ‘ 𝑘 ) = ⊥ )
23	22	fveq1d	⊢ ( 𝑘 = 𝐾 → ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) = ( ⊥ ‘ { 𝑑 } ) )
24	20 23	ineq12d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) )
25	19	oveqd	⊢ ( 𝑘 = 𝐾 → ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) = ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) )
26	25 23	ineq12d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) )
27	24 26	eqeq12d	⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ↔ ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) ) )
28	17 27	raleqbidv	⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ↔ ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) ) )
29	17 28	raleqbidv	⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ↔ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) ) )
30	14 29	rabeqbidv	⊢ ( 𝑘 = 𝐾 → { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } = { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } )
31	11 30	mpteq12dv	⊢ ( 𝑘 = 𝐾 → ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )
32		df-trnN	⊢ Trn = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) )
33	31 32 1	mptfvmpt	⊢ ( 𝐾 ∈ V → ( Trn ‘ 𝐾 ) = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )
34	8 33	syl5eq	⊢ ( 𝐾 ∈ V → 𝑇 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )
35	9 34	syl	⊢ ( 𝐾 ∈ 𝐶 → 𝑇 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )