Metamath Proof Explorer

Theorem tgrpset

Description: The translation group for a fiducial co-atom W . (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses tgrpset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tgrpset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tgrpset.g ⊢ 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
Assertion tgrpset ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑇 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )

Proof

Step Hyp Ref Expression
1 tgrpset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tgrpset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tgrpset.g ⊢ 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
4 1 tgrpfset ⊢ ( 𝐾 ∈ 𝑉 → ( TGrp ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) )
5 4 fveq1d ⊢ ( 𝐾 ∈ 𝑉 → ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) ‘ 𝑊 ) )
6 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
7 6 opeq2d ⊢ ( 𝑤 = 𝑊 → ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ )
8 eqidd ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∘ 𝑔 ) = ( 𝑓 ∘ 𝑔 ) )
9 6 6 8 mpoeq123dv ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) )
10 9 opeq2d ⊢ ( 𝑤 = 𝑊 → ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ )
11 7 10 preq12d ⊢ ( 𝑤 = 𝑊 → { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )
12 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) = ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )
13 prex ⊢ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ∈ V
14 11 12 13 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) ‘ 𝑊 ) = { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )
15 2 opeq2i ⊢ ⟨ ( Base ‘ ndx ) , 𝑇 ⟩ = ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩
16 eqid ⊢ ( 𝑓 ∘ 𝑔 ) = ( 𝑓 ∘ 𝑔 )
17 2 2 16 mpoeq123i ⊢ ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) )
18 17 opeq2i ⊢ ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩
19 15 18 preq12i ⊢ { ⟨ ( Base ‘ ndx ) , 𝑇 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ }
20 14 19 eqtr4di ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) ‘ 𝑊 ) = { ⟨ ( Base ‘ ndx ) , 𝑇 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )
21 5 20 sylan9eq ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) = { ⟨ ( Base ‘ ndx ) , 𝑇 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )
22 3 21 syl5eq ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑇 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )