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 ⊢ Y = R ↑ 𝑠 I
pws1.o ⊢ 1 ˙ = 1 R
Assertion pws1 ⊢ R ∈ Ring ∧ I ∈ V → I × 1 ˙ = 1 Y

Proof

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