Metamath Proof Explorer


Theorem dvaabl

Description: The constructed partial vector space A for a lattice K is an abelian group. (Contributed by NM, 11-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvalvec.h 𝐻 = ( LHyp ‘ 𝐾 )
dvalvec.v 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
Assertion dvaabl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ Abel )

Proof

Step Hyp Ref Expression
1 dvalvec.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dvalvec.v 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
3 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
6 1 3 4 5 2 dvaset ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 = ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) )
7 eqid ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
8 1 3 7 tgrpset ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) = { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } )
9 1 7 tgrpabl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) ∈ Abel )
10 8 9 eqeltrrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ∈ Abel )
11 fvex ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
12 eqid { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ }
13 12 grpbase ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ) )
14 eqid ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } )
15 14 lmodbase ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) ) )
16 13 15 eqtr3d ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V → ( Base ‘ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) ) )
17 11 16 ax-mp ( Base ‘ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) )
18 11 11 mpoex ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ∈ V
19 12 grpplusg ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ∈ V → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ) )
20 14 lmodplusg ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ∈ V → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) ) )
21 19 20 eqtr3d ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ∈ V → ( +g ‘ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) ) )
22 18 21 ax-mp ( +g ‘ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) )
23 17 22 ablprop ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ } ∈ Abel ↔ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) ∈ Abel )
24 10 23 sylib ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠𝑓 ) ) ⟩ } ) ∈ Abel )
25 6 24 eqeltrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ Abel )