Metamath Proof Explorer

Theorem zlmtset

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

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 5re 
 |-  5 e. RR
5 5lt9 
 |-  5 < 9
6 4 5 gtneii 
 |-  9 =/= 5
7 tsetndx 
 |-  ( TopSet ` ndx ) = 9
8 scandx 
 |-  ( Scalar ` ndx ) = 5
9 7 8 neeq12i 
 |-  ( ( TopSet ` ndx ) =/= ( Scalar ` ndx ) <-> 9 =/= 5 )
10 6 9 mpbir 
 |-  ( TopSet ` ndx ) =/= ( Scalar ` ndx )
11 3 10 setsnid 
 |-  ( TopSet ` G ) = ( TopSet ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
12 6re 
 |-  6 e. RR
13 6lt9 
 |-  6 < 9
14 12 13 gtneii 
 |-  9 =/= 6
15 vscandx 
 |-  ( .s ` ndx ) = 6
16 7 15 neeq12i 
 |-  ( ( TopSet ` ndx ) =/= ( .s ` ndx ) <-> 9 =/= 6 )
17 14 16 mpbir 
 |-  ( TopSet ` ndx ) =/= ( .s ` ndx )
18 3 17 setsnid 
 |-  ( TopSet ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( TopSet ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
19 2 11 18 3eqtri 
 |-  J = ( TopSet ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
20 eqid 
 |-  ( .g ` G ) = ( .g ` G )
21 1 20 zlmval 
 |-  ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
22 21 fveq2d 
 |-  ( G e. V -> ( TopSet ` W ) = ( TopSet ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
23 19 22 eqtr4id 
 |-  ( G e. V -> J = ( TopSet ` W ) )