Metamath Proof Explorer


Theorem plusfreseq

Description: If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020)

Ref Expression
Hypotheses plusfreseq.1 𝐵 = ( Base ‘ 𝑀 )
plusfreseq.2 + = ( +g𝑀 )
plusfreseq.3 = ( +𝑓𝑀 )
Assertion plusfreseq ( ∅ ∉ ran → ( + ↾ ( 𝐵 × 𝐵 ) ) = )

Proof

Step Hyp Ref Expression
1 plusfreseq.1 𝐵 = ( Base ‘ 𝑀 )
2 plusfreseq.2 + = ( +g𝑀 )
3 plusfreseq.3 = ( +𝑓𝑀 )
4 1 3 plusffn Fn ( 𝐵 × 𝐵 )
5 fnfun ( Fn ( 𝐵 × 𝐵 ) → Fun )
6 4 5 ax-mp Fun
7 6 a1i ( ∅ ∉ ran → Fun )
8 id ( ∅ ∉ ran → ∅ ∉ ran )
9 1 2 3 plusfval ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥 𝑦 ) = ( 𝑥 + 𝑦 ) )
10 9 eqcomd ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑦 ) )
11 10 rgen2 𝑥𝐵𝑦𝐵 ( 𝑥 + 𝑦 ) = ( 𝑥 𝑦 )
12 11 a1i ( ∅ ∉ ran → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 + 𝑦 ) = ( 𝑥 𝑦 ) )
13 fveq2 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( +𝑝 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14 df-ov ( 𝑥 + 𝑦 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ )
15 13 14 eqtr4di ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( +𝑝 ) = ( 𝑥 + 𝑦 ) )
16 fveq2 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ) = ( ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
17 df-ov ( 𝑥 𝑦 ) = ( ‘ ⟨ 𝑥 , 𝑦 ⟩ )
18 16 17 eqtr4di ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ) = ( 𝑥 𝑦 ) )
19 15 18 eqeq12d ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( +𝑝 ) = ( 𝑝 ) ↔ ( 𝑥 + 𝑦 ) = ( 𝑥 𝑦 ) ) )
20 19 ralxp ( ∀ 𝑝 ∈ ( 𝐵 × 𝐵 ) ( +𝑝 ) = ( 𝑝 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 + 𝑦 ) = ( 𝑥 𝑦 ) )
21 12 20 sylibr ( ∅ ∉ ran → ∀ 𝑝 ∈ ( 𝐵 × 𝐵 ) ( +𝑝 ) = ( 𝑝 ) )
22 fndm ( Fn ( 𝐵 × 𝐵 ) → dom = ( 𝐵 × 𝐵 ) )
23 22 eqcomd ( Fn ( 𝐵 × 𝐵 ) → ( 𝐵 × 𝐵 ) = dom )
24 4 23 ax-mp ( 𝐵 × 𝐵 ) = dom
25 24 fveqressseq ( ( Fun ∧ ∅ ∉ ran ∧ ∀ 𝑝 ∈ ( 𝐵 × 𝐵 ) ( +𝑝 ) = ( 𝑝 ) ) → ( + ↾ ( 𝐵 × 𝐵 ) ) = )
26 7 8 21 25 syl3anc ( ∅ ∉ ran → ( + ↾ ( 𝐵 × 𝐵 ) ) = )