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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐾 ∈ V → 𝑇 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )
35 9 34 syl ⊢ ( 𝐾 ∈ 𝐶 → 𝑇 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ ( 𝐿 ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( 𝑊 ‘ 𝑑 ) ∀ 𝑟 ∈ ( 𝑊 ‘ 𝑑 ) ( ( 𝑞 + ( 𝑓 ‘ 𝑞 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) = ( ( 𝑟 + ( 𝑓 ‘ 𝑟 ) ) ∩ ( ⊥ ‘ { 𝑑 } ) ) } ) )