Metamath Proof Explorer

Theorem ringinvval

Description: The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017)

Ref Expression
Hypotheses ringinvval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringinvval.p ⊢ ∗ = ( .r ‘ 𝑅 )
ringinvval.o ⊢ 1 = ( 1r ‘ 𝑅 )
ringinvval.n ⊢ 𝑁 = ( invr ‘ 𝑅 )
ringinvval.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion ringinvval ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 ringinvval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringinvval.p ⊢ ∗ = ( .r ‘ 𝑅 )
3 ringinvval.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 ringinvval.n ⊢ 𝑁 = ( invr ‘ 𝑅 )
5 ringinvval.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
6 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
7 5 6 unitgrpbas ⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
8 5 fvexi ⊢ 𝑈 ∈ V
9 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
10 9 2 mgpplusg ⊢ ∗ = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
11 6 10 ressplusg ⊢ ( 𝑈 ∈ V → ∗ = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
12 8 11 ax-mp ⊢ ∗ = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
13 eqid ⊢ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
14 5 6 4 invrfval ⊢ 𝑁 = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
15 7 12 13 14 grpinvval ⊢ ( 𝑋 ∈ 𝑈 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) ) )
16 15 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) ) )
17 5 6 3 unitgrpid ⊢ ( 𝑅 ∈ Ring → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
18 17 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈 ) → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
19 18 eqeq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈 ) → ( ( 𝑦 ∗ 𝑋 ) = 1 ↔ ( 𝑦 ∗ 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) ) )
20 19 riotabidva ⊢ ( 𝑅 ∈ Ring → ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = 1 ) = ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) ) )
21 20 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = 1 ) = ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) ) )
22 16 21 eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝑈 ( 𝑦 ∗ 𝑋 ) = 1 ) )