pws0g

Description: The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsmnd.y	$⊢ Y = R ↑_{𝑠} I$
	pws0g.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	pws0g	$⊢ (R \in Mnd \land I \in V) \to I \times \{\underset{˙}{0}\} = 0_{Y}$

Proof

Step	Hyp	Ref	Expression
1		pwsmnd.y	$⊢ Y = R ↑_{𝑠} I$
2		pws0g.z	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
4		simpr	$⊢ (R \in Mnd \land I \in V) \to I \in V$
5		fvexd	$⊢ (R \in Mnd \land I \in V) \to Scalar (R) \in V$
6		fconst6g	$⊢ R \in Mnd \to (I \times \{R\}) : I ⟶ Mnd$
7	6	adantr	$⊢ (R \in Mnd \land I \in V) \to (I \times \{R\}) : I ⟶ Mnd$
8	3 4 5 7	prds0g	$⊢ (R \in Mnd \land I \in V) \to 0_{𝑔} \circ (I \times \{R\}) = 0_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
9		fconstmpt	$⊢ I \times \{\underset{˙}{0}\} = (x \in I ⟼ \underset{˙}{0})$
10		elex	$⊢ R \in Mnd \to R \in V$
11	10	ad2antrr	$⊢ ((R \in Mnd \land I \in V) \land x \in I) \to R \in V$
12		fconstmpt	$⊢ I \times \{R\} = (x \in I ⟼ R)$
13	12	a1i	$⊢ (R \in Mnd \land I \in V) \to I \times \{R\} = (x \in I ⟼ R)$
14		fn0g	$⊢ 0_{𝑔} Fn V$
15	14	a1i	$⊢ (R \in Mnd \land I \in V) \to 0_{𝑔} Fn V$
16		dffn5	$⊢ 0_{𝑔} Fn V \leftrightarrow 0_{𝑔} = (r \in V ⟼ 0_{r})$
17	15 16	sylib	$⊢ (R \in Mnd \land I \in V) \to 0_{𝑔} = (r \in V ⟼ 0_{r})$
18		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
19	18 2	eqtr4di	$⊢ r = R \to 0_{r} = \underset{˙}{0}$
20	11 13 17 19	fmptco	$⊢ (R \in Mnd \land I \in V) \to 0_{𝑔} \circ (I \times \{R\}) = (x \in I ⟼ \underset{˙}{0})$
21	9 20	eqtr4id	$⊢ (R \in Mnd \land I \in V) \to I \times \{\underset{˙}{0}\} = 0_{𝑔} \circ (I \times \{R\})$
22		eqid	$⊢ Scalar (R) = Scalar (R)$
23	1 22	pwsval	$⊢ (R \in Mnd \land I \in V) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
24	23	fveq2d	$⊢ (R \in Mnd \land I \in V) \to 0_{Y} = 0_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
25	8 21 24	3eqtr4d	$⊢ (R \in Mnd \land I \in V) \to I \times \{\underset{˙}{0}\} = 0_{Y}$

Metamath Proof Explorer

Theorem pws0g

Proof