Metamath Proof Explorer


Theorem prds1

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