Metamath Proof Explorer

Theorem plusffval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses plusffval.1 âŠĒ ðĩ = ( Base ‘ 𝐚 )
plusffval.2 âŠĒ + = ( +g ‘ 𝐚 )
plusffval.3 âŠĒ âĻĢ = ( +𝑓 ‘ 𝐚 )
Assertion plusffval âĻĢ = ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) )

Proof

Step Hyp Ref Expression
1 plusffval.1 âŠĒ ðĩ = ( Base ‘ 𝐚 )
2 plusffval.2 âŠĒ + = ( +g ‘ 𝐚 )
3 plusffval.3 âŠĒ âĻĢ = ( +𝑓 ‘ 𝐚 )
4 fveq2 âŠĒ ( 𝑔 = 𝐚 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐚 ) )
5 4 1 eqtr4di âŠĒ ( 𝑔 = 𝐚 → ( Base ‘ 𝑔 ) = ðĩ )
6 fveq2 âŠĒ ( 𝑔 = 𝐚 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐚 ) )
7 6 2 eqtr4di âŠĒ ( 𝑔 = 𝐚 → ( +g ‘ 𝑔 ) = + )
8 7 oveqd âŠĒ ( 𝑔 = 𝐚 → ( ð‘Ĩ ( +g ‘ 𝑔 ) ð‘Ķ ) = ( ð‘Ĩ + ð‘Ķ ) )
9 5 5 8 mpoeq123dv âŠĒ ( 𝑔 = 𝐚 → ( ð‘Ĩ ∈ ( Base ‘ 𝑔 ) , ð‘Ķ ∈ ( Base ‘ 𝑔 ) â†Ķ ( ð‘Ĩ ( +g ‘ 𝑔 ) ð‘Ķ ) ) = ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) ) )
10 df-plusf âŠĒ +𝑓 = ( 𝑔 ∈ V â†Ķ ( ð‘Ĩ ∈ ( Base ‘ 𝑔 ) , ð‘Ķ ∈ ( Base ‘ 𝑔 ) â†Ķ ( ð‘Ĩ ( +g ‘ 𝑔 ) ð‘Ķ ) ) )
11 1 fvexi âŠĒ ðĩ ∈ V
12 2 fvexi âŠĒ + ∈ V
13 12 rnex âŠĒ ran + ∈ V
14 p0ex âŠĒ { ∅ } ∈ V
15 13 14 unex âŠĒ ( ran + ∊ { ∅ } ) ∈ V
16 df-ov âŠĒ ( ð‘Ĩ + ð‘Ķ ) = ( + ‘ âŸĻ ð‘Ĩ , ð‘Ķ âŸĐ )
17 fvrn0 âŠĒ ( + ‘ âŸĻ ð‘Ĩ , ð‘Ķ âŸĐ ) ∈ ( ran + ∊ { ∅ } )
18 16 17 eqeltri âŠĒ ( ð‘Ĩ + ð‘Ķ ) ∈ ( ran + ∊ { ∅ } )
19 18 rgen2w âŠĒ ∀ ð‘Ĩ ∈ ðĩ ∀ ð‘Ķ ∈ ðĩ ( ð‘Ĩ + ð‘Ķ ) ∈ ( ran + ∊ { ∅ } )
20 11 11 15 19 mpoexw âŠĒ ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) ) ∈ V
21 9 10 20 fvmpt âŠĒ ( 𝐚 ∈ V → ( +𝑓 ‘ 𝐚 ) = ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) ) )
22 fvprc âŠĒ ( ÂŽ 𝐚 ∈ V → ( +𝑓 ‘ 𝐚 ) = ∅ )
23 fvprc âŠĒ ( ÂŽ 𝐚 ∈ V → ( Base ‘ 𝐚 ) = ∅ )
24 1 23 eqtrid âŠĒ ( ÂŽ 𝐚 ∈ V → ðĩ = ∅ )
25 24 olcd âŠĒ ( ÂŽ 𝐚 ∈ V → ( ðĩ = ∅ âˆĻ ðĩ = ∅ ) )
26 0mpo0 âŠĒ ( ( ðĩ = ∅ âˆĻ ðĩ = ∅ ) → ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) ) = ∅ )
27 25 26 syl âŠĒ ( ÂŽ 𝐚 ∈ V → ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) ) = ∅ )
28 22 27 eqtr4d âŠĒ ( ÂŽ 𝐚 ∈ V → ( +𝑓 ‘ 𝐚 ) = ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) ) )
29 21 28 pm2.61i âŠĒ ( +𝑓 ‘ 𝐚 ) = ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) )
30 3 29 eqtri âŠĒ âĻĢ = ( ð‘Ĩ ∈ ðĩ , ð‘Ķ ∈ ðĩ â†Ķ ( ð‘Ĩ + ð‘Ķ ) )