Metamath Proof Explorer

Theorem istlm

Description: The predicate " W is a topological left module". (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses istlm.s ⊢ · = ( ·sf ‘ 𝑊 )
istlm.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
istlm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
istlm.k ⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
Assertion istlm ( 𝑊 ∈ TopMod ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 istlm.s ⊢ · = ( ·sf ‘ 𝑊 )
2 istlm.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3 istlm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 istlm.k ⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
5 anass ⊢ ( ( ( 𝑊 ∈ ( TopMnd ∩ LMod ) ∧ 𝐹 ∈ TopRing ) ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) ↔ ( 𝑊 ∈ ( TopMnd ∩ LMod ) ∧ ( 𝐹 ∈ TopRing ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) ) )
6 df-3an ⊢ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ) ∧ 𝐹 ∈ TopRing ) )
7 elin ⊢ ( 𝑊 ∈ ( TopMnd ∩ LMod ) ↔ ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ) )
8 7 anbi1i ⊢ ( ( 𝑊 ∈ ( TopMnd ∩ LMod ) ∧ 𝐹 ∈ TopRing ) ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ) ∧ 𝐹 ∈ TopRing ) )
9 6 8 bitr4i ⊢ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ↔ ( 𝑊 ∈ ( TopMnd ∩ LMod ) ∧ 𝐹 ∈ TopRing ) )
10 9 anbi1i ⊢ ( ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) ↔ ( ( 𝑊 ∈ ( TopMnd ∩ LMod ) ∧ 𝐹 ∈ TopRing ) ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) )
11 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
12 11 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
13 12 eleq1d ⊢ ( 𝑤 = 𝑊 → ( ( Scalar ‘ 𝑤 ) ∈ TopRing ↔ 𝐹 ∈ TopRing ) )
14 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·sf ‘ 𝑤 ) = ( ·sf ‘ 𝑊 ) )
15 14 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·sf ‘ 𝑤 ) = · )
16 12 fveq2d ⊢ ( 𝑤 = 𝑊 → ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) = ( TopOpen ‘ 𝐹 ) )
17 16 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) = 𝐾 )
18 fveq2 ⊢ ( 𝑤 = 𝑊 → ( TopOpen ‘ 𝑤 ) = ( TopOpen ‘ 𝑊 ) )
19 18 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( TopOpen ‘ 𝑤 ) = 𝐽 )
20 17 19 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) = ( 𝐾 ×t 𝐽 ) )
21 20 19 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) = ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
22 15 21 eleq12d ⊢ ( 𝑤 = 𝑊 → ( ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ↔ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) )
23 13 22 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) ↔ ( 𝐹 ∈ TopRing ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) ) )
24 df-tlm ⊢ TopMod = { 𝑤 ∈ ( TopMnd ∩ LMod ) ∣ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) }
25 23 24 elrab2 ⊢ ( 𝑊 ∈ TopMod ↔ ( 𝑊 ∈ ( TopMnd ∩ LMod ) ∧ ( 𝐹 ∈ TopRing ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) ) )
26 5 10 25 3bitr4ri ⊢ ( 𝑊 ∈ TopMod ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) )