istlm

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

	Ref	Expression
Hypotheses	istlm.s	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
	istlm.j	$⊢ J = TopOpen (W)$
	istlm.f	$⊢ F = Scalar (W)$
	istlm.k	$⊢ K = TopOpen (F)$
Assertion	istlm	$⊢ W \in TopMod \leftrightarrow ((W \in TopMnd \land W \in LMod \land F \in TopRing) \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J))$

Proof

Step	Hyp	Ref	Expression
1		istlm.s	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
2		istlm.j	$⊢ J = TopOpen (W)$
3		istlm.f	$⊢ F = Scalar (W)$
4		istlm.k	$⊢ K = TopOpen (F)$
5		anass	$⊢ ((W \in (TopMnd \cap LMod) \land F \in TopRing) \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)) \leftrightarrow (W \in (TopMnd \cap LMod) \land (F \in TopRing \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)))$
6		df-3an	$⊢ (W \in TopMnd \land W \in LMod \land F \in TopRing) \leftrightarrow ((W \in TopMnd \land W \in LMod) \land F \in TopRing)$
7		elin	$⊢ W \in (TopMnd \cap LMod) \leftrightarrow (W \in TopMnd \land W \in LMod)$
8	7	anbi1i	$⊢ (W \in (TopMnd \cap LMod) \land F \in TopRing) \leftrightarrow ((W \in TopMnd \land W \in LMod) \land F \in TopRing)$
9	6 8	bitr4i	$⊢ (W \in TopMnd \land W \in LMod \land F \in TopRing) \leftrightarrow (W \in (TopMnd \cap LMod) \land F \in TopRing)$
10	9	anbi1i	$⊢ ((W \in TopMnd \land W \in LMod \land F \in TopRing) \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)) \leftrightarrow ((W \in (TopMnd \cap LMod) \land F \in TopRing) \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J))$
11		fveq2	$⊢ w = W \to Scalar (w) = Scalar (W)$
12	11 3	eqtr4di	$⊢ w = W \to Scalar (w) = F$
13	12	eleq1d	$⊢ w = W \to (Scalar (w) \in TopRing \leftrightarrow F \in TopRing)$
14		fveq2	$⊢ w = W \to \cdot_{𝑠𝑓} (w) = \cdot_{𝑠𝑓} (W)$
15	14 1	eqtr4di	$⊢ w = W \to \cdot_{𝑠𝑓} (w) = \underset{˙}{\cdot}$
16	12	fveq2d	$⊢ w = W \to TopOpen (Scalar (w)) = TopOpen (F)$
17	16 4	eqtr4di	$⊢ w = W \to TopOpen (Scalar (w)) = K$
18		fveq2	$⊢ w = W \to TopOpen (w) = TopOpen (W)$
19	18 2	eqtr4di	$⊢ w = W \to TopOpen (w) = J$
20	17 19	oveq12d	$⊢ w = W \to TopOpen (Scalar (w)) \times_{t} TopOpen (w) = K \times_{t} J$
21	20 19	oveq12d	$⊢ w = W \to (TopOpen (Scalar (w)) \times_{t} TopOpen (w)) Cn TopOpen (w) = (K \times_{t} J) Cn J$
22	15 21	eleq12d	$⊢ w = W \to (\cdot_{𝑠𝑓} (w) \in ((TopOpen (Scalar (w)) \times_{t} TopOpen (w)) Cn TopOpen (w)) \leftrightarrow \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J))$
23	13 22	anbi12d	$⊢ w = W \to ((Scalar (w) \in TopRing \land \cdot_{𝑠𝑓} (w) \in ((TopOpen (Scalar (w)) \times_{t} TopOpen (w)) Cn TopOpen (w))) \leftrightarrow (F \in TopRing \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)))$
24		df-tlm	$⊢ TopMod = \{w \in (TopMnd \cap LMod) \| (Scalar (w) \in TopRing \land \cdot_{𝑠𝑓} (w) \in ((TopOpen (Scalar (w)) \times_{t} TopOpen (w)) Cn TopOpen (w)))\}$
25	23 24	elrab2	$⊢ W \in TopMod \leftrightarrow (W \in (TopMnd \cap LMod) \land (F \in TopRing \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)))$
26	5 10 25	3bitr4ri	$⊢ W \in TopMod \leftrightarrow ((W \in TopMnd \land W \in LMod \land F \in TopRing) \land \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J))$

Metamath Proof Explorer

Theorem istlm

Proof