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 ‘ 𝐿 ) )