Metamath Proof Explorer

Theorem zlmtsetOLD

Description: Obsolete proof of zlmtset as of 11-Nov-2024. Topology in a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses zlmlem2.1 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
zlmtset.1 ⊢ 𝐽 = ( TopSet ‘ 𝐺 )
Assertion zlmtsetOLD ( 𝐺 ∈ 𝑉 → 𝐽 = ( TopSet ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 zlmlem2.1 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2 zlmtset.1 ⊢ 𝐽 = ( TopSet ‘ 𝐺 )
3 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
4 5re ⊢ 5 ∈ ℝ
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 ‘ 𝐺 ) = ( TopSet ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
12 6re ⊢ 6 ∈ ℝ
13 6lt9 ⊢ 6 < 9
14 12 13 gtneii ⊢ 9 ≠ 6
15 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
16 7 15 neeq12i ⊢ ( ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ 9 ≠ 6 )
17 14 16 mpbir ⊢ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
18 3 17 setsnid ⊢ ( TopSet ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
19 2 11 18 3eqtri ⊢ 𝐽 = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
20 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
21 1 20 zlmval ⊢ ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
22 21 fveq2d ⊢ ( 𝐺 ∈ 𝑉 → ( TopSet ‘ 𝑊 ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) ) )
23 19 22 eqtr4id ⊢ ( 𝐺 ∈ 𝑉 → 𝐽 = ( TopSet ‘ 𝑊 ) )