Metamath Proof Explorer

Theorem invginvrid

Description: Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018)

Ref Expression
Hypotheses invginvrid.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
invginvrid.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
invginvrid.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
invginvrid.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
invginvrid.t ⊢ · = ( .r ‘ 𝑅 )
Assertion invginvrid ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝑌 ) · ( ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) · 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 invginvrid.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 invginvrid.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 invginvrid.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
4 invginvrid.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
5 invginvrid.t ⊢ · = ( .r ‘ 𝑅 )
6 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
7 6 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
8 7 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
9 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
10 1 2 unitcl ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ 𝐵 )
11 1 3 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
12 9 10 11 syl2an ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
13 12 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
14 2 3 unitnegcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝑈 )
15 2 4 1 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝑈 ) → ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 )
16 14 15 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 )
17 16 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 )
18 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
19 6 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
20 6 5 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
21 19 20 mndass ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑁 ‘ 𝑌 ) · ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ) · 𝑋 ) = ( ( 𝑁 ‘ 𝑌 ) · ( ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) · 𝑋 ) ) )
22 21 eqcomd ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 ‘ 𝑌 ) · ( ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) · 𝑋 ) ) = ( ( ( 𝑁 ‘ 𝑌 ) · ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ) · 𝑋 ) )
23 8 13 17 18 22 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝑌 ) · ( ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) · 𝑋 ) ) = ( ( ( 𝑁 ‘ 𝑌 ) · ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ) · 𝑋 ) )
24 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑅 ∈ Ring )
25 14 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝑈 )
26 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
27 2 4 5 26 unitrinv ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝑌 ) · ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ) = ( 1r ‘ 𝑅 ) )
28 24 25 27 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝑌 ) · ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ) = ( 1r ‘ 𝑅 ) )
29 28 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝑁 ‘ 𝑌 ) · ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
30 1 5 26 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
31 30 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
32 23 29 31 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝑌 ) · ( ( 𝐼 ‘ ( 𝑁 ‘ 𝑌 ) ) · 𝑋 ) ) = 𝑋 )