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 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
zlmtset.1 ⊢ 𝐽 = ( TopSet ‘ 𝐺 )
Assertion zlmtset ( 𝐺 ∈ 𝑉 → 𝐽 = ( TopSet ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 zlmlem2.1 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2 zlmtset.1 ⊢ 𝐽 = ( TopSet ‘ 𝐺 )
3 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
4 slotstnscsi ⊢ ( ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
5 4 simp1i ⊢ ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx )
6 3 5 setsnid ⊢ ( TopSet ‘ 𝐺 ) = ( TopSet ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
7 4 simp2i ⊢ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
8 3 7 setsnid ⊢ ( TopSet ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
9 2 6 8 3eqtri ⊢ 𝐽 = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
10 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
11 1 10 zlmval ⊢ ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
12 11 fveq2d ⊢ ( 𝐺 ∈ 𝑉 → ( TopSet ‘ 𝑊 ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) ) )
13 9 12 eqtr4id ⊢ ( 𝐺 ∈ 𝑉 → 𝐽 = ( TopSet ‘ 𝑊 ) )