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 ) , ( 𝑓𝑇 , 𝑔𝑇 ↦ ( 𝑓𝑔 ) ) ⟩ } )