Theorem pws1

Description: Value of the ring unit 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 ‘ 𝑌 ) )