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 sseldi ⊢ ( ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 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 sseldi ⊢ ( ¬ ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 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 syl5eq ⊢ ( ¬ 𝐺 ∈ 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 ) )