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

Metamath Proof Explorer

Theorem pws1

Description: Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses pws1.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pws1.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion pws1 ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 1 } ) = ( 1r ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pws1.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pws1.o ⊢ 1 = ( 1r ‘ 𝑅 )
3 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
4 1 3 pwsval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
5 4 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 1r ‘ 𝑌 ) = ( 1r ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
6 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
7 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
8 fvexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) ∈ V )
9 fconst6g ⊢ ( 𝑅 ∈ Ring → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Ring )
10 9 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Ring )
11 6 7 8 10 prds1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 1r ∘ ( 𝐼 × { 𝑅 } ) ) = ( 1r ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
12 fn0g ⊢ 0g Fn V
13 fnmgp ⊢ mulGrp Fn V
14 ssv ⊢ ran mulGrp ⊆ V
15 14 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran mulGrp ⊆ V )
16 fnco ⊢ ( ( 0g Fn V ∧ mulGrp Fn V ∧ ran mulGrp ⊆ V ) → ( 0g ∘ mulGrp ) Fn V )
17 12 13 15 16 mp3an12i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 0g ∘ mulGrp ) Fn V )
18 df-ur ⊢ 1r = ( 0g ∘ mulGrp )
19 18 fneq1i ⊢ ( 1r Fn V ↔ ( 0g ∘ mulGrp ) Fn V )
20 17 19 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 1r Fn V )
21 elex ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ V )
22 21 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 ∈ V )
23 fcoconst ⊢ ( ( 1r Fn V ∧ 𝑅 ∈ V ) → ( 1r ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) )
24 20 22 23 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 1r ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) )
25 2 sneqi ⊢ { 1 } = { ( 1r ‘ 𝑅 ) }
26 25 xpeq2i ⊢ ( 𝐼 × { 1 } ) = ( 𝐼 × { ( 1r ‘ 𝑅 ) } )
27 24 26 eqtr4di ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 1r ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { 1 } ) )
28 5 11 27 3eqtr2rd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 1 } ) = ( 1r ‘ 𝑌 ) )