Metamath Proof Explorer

Theorem prds1

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

Ref Expression
Hypotheses prds1.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prds1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prds1.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prds1.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Ring )
Assertion prds1 ( 𝜑 → ( 1r ∘ 𝑅 ) = ( 1r ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 prds1.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prds1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3 prds1.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prds1.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Ring )
5 eqid ⊢ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) = ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) )
6 mgpf ⊢ ( mulGrp ↾ Ring ) : Ring ⟶ Mnd
7 fco2 ⊢ ( ( ( mulGrp ↾ Ring ) : Ring ⟶ Mnd ∧ 𝑅 : 𝐼 ⟶ Ring ) → ( mulGrp ∘ 𝑅 ) : 𝐼 ⟶ Mnd )
8 6 4 7 sylancr ⊢ ( 𝜑 → ( mulGrp ∘ 𝑅 ) : 𝐼 ⟶ Mnd )
9 5 2 3 8 prds0g ⊢ ( 𝜑 → ( 0g ∘ ( mulGrp ∘ 𝑅 ) ) = ( 0g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
10 eqidd ⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) ) )
11 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
12 4 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
13 1 11 5 2 3 12 prdsmgp ⊢ ( 𝜑 → ( ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) ∧ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) ) )
14 13 simpld ⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
15 13 simprd ⊢ ( 𝜑 → ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
16 15 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ∧ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑌 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) 𝑦 ) )
17 10 14 16 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝑌 ) ) = ( 0g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
18 9 17 eqtr4d ⊢ ( 𝜑 → ( 0g ∘ ( mulGrp ∘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑌 ) ) )
19 df-ur ⊢ 1r = ( 0g ∘ mulGrp )
20 19 coeq1i ⊢ ( 1r ∘ 𝑅 ) = ( ( 0g ∘ mulGrp ) ∘ 𝑅 )
21 coass ⊢ ( ( 0g ∘ mulGrp ) ∘ 𝑅 ) = ( 0g ∘ ( mulGrp ∘ 𝑅 ) )
22 20 21 eqtri ⊢ ( 1r ∘ 𝑅 ) = ( 0g ∘ ( mulGrp ∘ 𝑅 ) )
23 eqid ⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ 𝑌 )
24 11 23 ringidval ⊢ ( 1r ‘ 𝑌 ) = ( 0g ‘ ( mulGrp ‘ 𝑌 ) )
25 18 22 24 3eqtr4g ⊢ ( 𝜑 → ( 1r ∘ 𝑅 ) = ( 1r ‘ 𝑌 ) )