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 ) )