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 
|- .x. = ( .sf ` W )
istlm.j 
|- J = ( TopOpen ` W )
istlm.f 
|- F = ( Scalar ` W )
istlm.k 
|- K = ( TopOpen ` F )
Assertion istlm 
|- ( W e. TopMod <-> ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) /\ .x. e. ( ( K tX J ) Cn J ) ) )

Proof

Step Hyp Ref Expression
1 istlm.s 
 |-  .x. = ( .sf ` W )
2 istlm.j 
 |-  J = ( TopOpen ` W )
3 istlm.f 
 |-  F = ( Scalar ` W )
4 istlm.k 
 |-  K = ( TopOpen ` F )
5 anass 
 |-  ( ( ( W e. ( TopMnd i^i LMod ) /\ F e. TopRing ) /\ .x. e. ( ( K tX J ) Cn J ) ) <-> ( W e. ( TopMnd i^i LMod ) /\ ( F e. TopRing /\ .x. e. ( ( K tX J ) Cn J ) ) ) )
6 df-3an 
 |-  ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) <-> ( ( W e. TopMnd /\ W e. LMod ) /\ F e. TopRing ) )
7 elin 
 |-  ( W e. ( TopMnd i^i LMod ) <-> ( W e. TopMnd /\ W e. LMod ) )
8 7 anbi1i 
 |-  ( ( W e. ( TopMnd i^i LMod ) /\ F e. TopRing ) <-> ( ( W e. TopMnd /\ W e. LMod ) /\ F e. TopRing ) )
9 6 8 bitr4i 
 |-  ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) <-> ( W e. ( TopMnd i^i LMod ) /\ F e. TopRing ) )
10 9 anbi1i 
 |-  ( ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) /\ .x. e. ( ( K tX J ) Cn J ) ) <-> ( ( W e. ( TopMnd i^i LMod ) /\ F e. TopRing ) /\ .x. e. ( ( K tX J ) Cn J ) ) )
11 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
12 11 3 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = F )
13 12 eleq1d 
 |-  ( w = W -> ( ( Scalar ` w ) e. TopRing <-> F e. TopRing ) )
14 fveq2 
 |-  ( w = W -> ( .sf ` w ) = ( .sf ` W ) )
15 14 1 eqtr4di 
 |-  ( w = W -> ( .sf ` w ) = .x. )
16 12 fveq2d 
 |-  ( w = W -> ( TopOpen ` ( Scalar ` w ) ) = ( TopOpen ` F ) )
17 16 4 eqtr4di 
 |-  ( w = W -> ( TopOpen ` ( Scalar ` w ) ) = K )
18 fveq2 
 |-  ( w = W -> ( TopOpen ` w ) = ( TopOpen ` W ) )
19 18 2 eqtr4di 
 |-  ( w = W -> ( TopOpen ` w ) = J )
20 17 19 oveq12d 
 |-  ( w = W -> ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) = ( K tX J ) )
21 20 19 oveq12d 
 |-  ( w = W -> ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) = ( ( K tX J ) Cn J ) )
22 15 21 eleq12d 
 |-  ( w = W -> ( ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) <-> .x. e. ( ( K tX J ) Cn J ) ) )
23 13 22 anbi12d 
 |-  ( w = W -> ( ( ( Scalar ` w ) e. TopRing /\ ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) ) <-> ( F e. TopRing /\ .x. e. ( ( K tX J ) Cn J ) ) ) )
24 df-tlm 
 |-  TopMod = { w e. ( TopMnd i^i LMod ) | ( ( Scalar ` w ) e. TopRing /\ ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) ) }
25 23 24 elrab2 
 |-  ( W e. TopMod <-> ( W e. ( TopMnd i^i LMod ) /\ ( F e. TopRing /\ .x. e. ( ( K tX J ) Cn J ) ) ) )
26 5 10 25 3bitr4ri 
 |-  ( W e. TopMod <-> ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) /\ .x. e. ( ( K tX J ) Cn J ) ) )