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 ⨣ → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ ) |