Metamath Proof Explorer


Theorem grpinvfvalALT

Description: Shorter proof of grpinvfval using ax-rep . (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses grpinvval.b 𝐵 = ( Base ‘ 𝐺 )
grpinvval.p + = ( +g𝐺 )
grpinvval.o 0 = ( 0g𝐺 )
grpinvval.n 𝑁 = ( invg𝐺 )
Assertion grpinvfvalALT 𝑁 = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 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 14 15 1 mptfvmpt ( 𝐺 ∈ V → ( invg𝐺 ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
17 fvprc ( ¬ 𝐺 ∈ V → ( invg𝐺 ) = ∅ )
18 mpt0 ( 𝑥 ∈ ∅ ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) = ∅
19 17 18 eqtr4di ( ¬ 𝐺 ∈ V → ( invg𝐺 ) = ( 𝑥 ∈ ∅ ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
20 fvprc ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
21 1 20 eqtrid ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
22 21 mpteq1d ( ¬ 𝐺 ∈ V → ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
23 19 22 eqtr4d ( ¬ 𝐺 ∈ V → ( invg𝐺 ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) ) )
24 16 23 pm2.61i ( invg𝐺 ) = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) )
25 4 24 eqtri 𝑁 = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 + 𝑥 ) = 0 ) )