Theorem zlmtset

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

	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		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 ‘ 𝑊 ) )