Theorem pws0g

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

	Ref	Expression
Hypotheses	pwsmnd.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pws0g.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	pws0g	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		pwsmnd.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pws0g.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
4		simpr	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
5		fvexd	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) ∈ V )
6		fconst6g	⊢ ( 𝑅 ∈ Mnd → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Mnd )
7	6	adantr	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Mnd )
8	3 4 5 7	prds0g	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 0g ∘ ( 𝐼 × { 𝑅 } ) ) = ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
9		fconstmpt	⊢ ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 )
10		elex	⊢ ( 𝑅 ∈ Mnd → 𝑅 ∈ V )
11	10	ad2antrr	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ V )
12		fconstmpt	⊢ ( 𝐼 × { 𝑅 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
13	12	a1i	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 𝑅 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
14		fn0g	⊢ 0g Fn V
15	14	a1i	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → 0g Fn V )
16		dffn5	⊢ ( 0g Fn V ↔ 0g = ( 𝑟 ∈ V ↦ ( 0g ‘ 𝑟 ) ) )
17	15 16	sylib	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → 0g = ( 𝑟 ∈ V ↦ ( 0g ‘ 𝑟 ) ) )
18		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
19	18 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
20	11 13 17 19	fmptco	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 0g ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) )
21	9 20	eqtr4id	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 0 } ) = ( 0g ∘ ( 𝐼 × { 𝑅 } ) ) )
22		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
23	1 22	pwsval	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
24	23	fveq2d	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 0g ‘ 𝑌 ) = ( 0g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
25	8 21 24	3eqtr4d	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ 𝑌 ) )