Metamath Proof Explorer


Theorem invrpropd

Description: The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014) (Revised by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses rngidpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
rngidpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
rngidpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion invrpropd ( 𝜑 → ( invr𝐾 ) = ( invr𝐿 ) )

Proof

Step Hyp Ref Expression
1 rngidpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 rngidpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 rngidpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
4 eqid ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
5 eqid ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) = ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) )
6 4 5 unitgrpbas ( Unit ‘ 𝐾 ) = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) )
7 6 a1i ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) )
8 1 2 3 unitpropd ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )
9 eqid ( Unit ‘ 𝐿 ) = ( Unit ‘ 𝐿 )
10 eqid ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) = ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) )
11 9 10 unitgrpbas ( Unit ‘ 𝐿 ) = ( Base ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) )
12 8 11 eqtrdi ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Base ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) ) )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 4 unitss ( Unit ‘ 𝐾 ) ⊆ ( Base ‘ 𝐾 )
15 14 1 sseqtrrid ( 𝜑 → ( Unit ‘ 𝐾 ) ⊆ 𝐵 )
16 15 sselda ( ( 𝜑𝑥 ∈ ( Unit ‘ 𝐾 ) ) → 𝑥𝐵 )
17 15 sselda ( ( 𝜑𝑦 ∈ ( Unit ‘ 𝐾 ) ) → 𝑦𝐵 )
18 16 17 anim12dan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ 𝐾 ) ∧ 𝑦 ∈ ( Unit ‘ 𝐾 ) ) ) → ( 𝑥𝐵𝑦𝐵 ) )
19 18 3 syldan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ 𝐾 ) ∧ 𝑦 ∈ ( Unit ‘ 𝐾 ) ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
20 fvex ( Unit ‘ 𝐾 ) ∈ V
21 eqid ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
22 eqid ( .r𝐾 ) = ( .r𝐾 )
23 21 22 mgpplusg ( .r𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
24 5 23 ressplusg ( ( Unit ‘ 𝐾 ) ∈ V → ( .r𝐾 ) = ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) )
25 20 24 ax-mp ( .r𝐾 ) = ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) )
26 25 oveqi ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) 𝑦 )
27 fvex ( Unit ‘ 𝐿 ) ∈ V
28 eqid ( mulGrp ‘ 𝐿 ) = ( mulGrp ‘ 𝐿 )
29 eqid ( .r𝐿 ) = ( .r𝐿 )
30 28 29 mgpplusg ( .r𝐿 ) = ( +g ‘ ( mulGrp ‘ 𝐿 ) )
31 10 30 ressplusg ( ( Unit ‘ 𝐿 ) ∈ V → ( .r𝐿 ) = ( +g ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) ) )
32 27 31 ax-mp ( .r𝐿 ) = ( +g ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) )
33 32 oveqi ( 𝑥 ( .r𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) ) 𝑦 )
34 19 26 33 3eqtr3g ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ 𝐾 ) ∧ 𝑦 ∈ ( Unit ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) ) 𝑦 ) )
35 7 12 34 grpinvpropd ( 𝜑 → ( invg ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) = ( invg ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) ) )
36 eqid ( invr𝐾 ) = ( invr𝐾 )
37 4 5 36 invrfval ( invr𝐾 ) = ( invg ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) )
38 eqid ( invr𝐿 ) = ( invr𝐿 )
39 9 10 38 invrfval ( invr𝐿 ) = ( invg ‘ ( ( mulGrp ‘ 𝐿 ) ↾s ( Unit ‘ 𝐿 ) ) )
40 35 37 39 3eqtr4g ( 𝜑 → ( invr𝐾 ) = ( invr𝐿 ) )