This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑌 ) )