Metamath Proof Explorer


Theorem grpinvfval

Description: The inverse function of a group. For a shorter proof using ax-rep , see grpinvfvalALT . (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses grpinvval.b 𝐵 = ( Base ‘ 𝐺 )
grpinvval.p + = ( +g𝐺 )
grpinvval.o 0 = ( 0g𝐺 )
grpinvval.n 𝑁 = ( invg𝐺 )
Assertion grpinvfval 𝑁 = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 grpinvval.b 𝐵 = ( Base ‘ 𝐺 )
2 grpinvval.p + = ( +g𝐺 )
3 grpinvval.o 0 = ( 0g𝐺 )
4 grpinvval.n 𝑁 = ( invg𝐺 )
5 fveq2 ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
7 fveq2 ( 𝑔 = 𝐺 → ( +g𝑔 ) = ( +g𝐺 ) )
8 7 2 eqtr4di ( 𝑔 = 𝐺 → ( +g𝑔 ) = + )
9 8 oveqd ( 𝑔 = 𝐺 → ( 𝑦 ( +g𝑔 ) 𝑥 ) = ( 𝑦 + 𝑥 ) )
10 fveq2 ( 𝑔 = 𝐺 → ( 0g𝑔 ) = ( 0g𝐺 ) )
11 10 3 eqtr4di ( 𝑔 = 𝐺 → ( 0g𝑔 ) = 0 )
12 9 11 eqeq12d ( 𝑔 = 𝐺 → ( ( 𝑦 ( +g𝑔 ) 𝑥 ) = ( 0g𝑔 ) ↔ ( 𝑦 + 𝑥 ) = 0 ) )
13 6 12 riotaeqbidv ( 𝑔 = 𝐺 → ( 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( +g𝑔 ) 𝑥 ) = ( 0g𝑔 ) ) = ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) )
14 6 13 mpteq12dv ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( +g𝑔 ) 𝑥 ) = ( 0g𝑔 ) ) ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
15 df-minusg invg = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( +g𝑔 ) 𝑥 ) = ( 0g𝑔 ) ) ) )
16 1 fvexi 𝐵 ∈ V
17 p0ex { ∅ } ∈ V
18 17 16 unex ( { ∅ } ∪ 𝐵 ) ∈ V
19 ssun2 𝐵 ⊆ ( { ∅ } ∪ 𝐵 )
20 riotacl ( ∃! 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 → ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ 𝐵 )
21 19 20 sselid ( ∃! 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 → ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ ( { ∅ } ∪ 𝐵 ) )
22 ssun1 { ∅ } ⊆ ( { ∅ } ∪ 𝐵 )
23 riotaund ( ¬ ∃! 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 → ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) = ∅ )
24 riotaex ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ V
25 24 elsn ( ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ { ∅ } ↔ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) = ∅ )
26 23 25 sylibr ( ¬ ∃! 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 → ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ { ∅ } )
27 22 26 sselid ( ¬ ∃! 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 → ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ ( { ∅ } ∪ 𝐵 ) )
28 21 27 pm2.61i ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ ( { ∅ } ∪ 𝐵 )
29 28 rgenw 𝑥𝐵 ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ∈ ( { ∅ } ∪ 𝐵 )
30 16 18 29 mptexw ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) ∈ V
31 14 15 30 fvmpt ( 𝐺 ∈ V → ( invg𝐺 ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
32 fvprc ( ¬ 𝐺 ∈ V → ( invg𝐺 ) = ∅ )
33 mpt0 ( 𝑥 ∈ ∅ ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) = ∅
34 32 33 eqtr4di ( ¬ 𝐺 ∈ V → ( invg𝐺 ) = ( 𝑥 ∈ ∅ ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
35 fvprc ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
36 1 35 eqtrid ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
37 36 mpteq1d ( ¬ 𝐺 ∈ V → ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
38 34 37 eqtr4d ( ¬ 𝐺 ∈ V → ( invg𝐺 ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
39 31 38 pm2.61i ( invg𝐺 ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) )
40 4 39 eqtri 𝑁 = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) )