Metamath Proof Explorer

Theorem zlmtset

Description: Topology in a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017) (Proof shortened by AV, 12-Nov-2024)

Ref Expression
Hypotheses zlmlem2.1 
|- W = ( ZMod ` G )
zlmtset.1 
|- J = ( TopSet ` G )
Assertion zlmtset 
|- ( G e. V -> J = ( TopSet ` W ) )

Proof

Step Hyp Ref Expression
1 zlmlem2.1 
 |-  W = ( ZMod ` G )
2 zlmtset.1 
 |-  J = ( TopSet ` G )
3 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
4 slotstnscsi 
 |-  ( ( TopSet ` ndx ) =/= ( Scalar ` ndx ) /\ ( TopSet ` ndx ) =/= ( .s ` ndx ) /\ ( TopSet ` ndx ) =/= ( .i ` ndx ) )
5 4 simp1i 
 |-  ( TopSet ` ndx ) =/= ( Scalar ` ndx )
6 3 5 setsnid 
 |-  ( TopSet ` G ) = ( TopSet ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
7 4 simp2i 
 |-  ( TopSet ` ndx ) =/= ( .s ` ndx )
8 3 7 setsnid 
 |-  ( TopSet ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( TopSet ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
9 2 6 8 3eqtri 
 |-  J = ( TopSet ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
10 eqid 
 |-  ( .g ` G ) = ( .g ` G )
11 1 10 zlmval 
 |-  ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
12 11 fveq2d 
 |-  ( G e. V -> ( TopSet ` W ) = ( TopSet ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
13 9 12 eqtr4id 
 |-  ( G e. V -> J = ( TopSet ` W ) )