Theorem addinvcom

Description: A number commutes with its additive inverse. Compare remulinvcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Hypotheses	addinvcom.a	$$⊢\phi \to A\in ℂ$$
	addinvcom.b	$$⊢\phi \to B\in ℂ$$
	addinvcom.1	$$⊢\phi \to A+B=0$$
Assertion	addinvcom	$$⊢\phi \to B+A=0$$

Proof

Step	Hyp	Ref	Expression
1		addinvcom.a	$$⊢\phi \to A\in ℂ$$
2		addinvcom.b	$$⊢\phi \to B\in ℂ$$
3		addinvcom.1	$$⊢\phi \to A+B=0$$
4		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
5		simpl	$$⊢\left(A+x=0\wedge x+A=0\right)\to A+x=0$$
6	5	rgenw	$$⊢\forall x\in ℂ\left(\left(A+x=0\wedge x+A=0\right)\to A+x=0\right)$$
7	6	a1i	$$⊢\phi \to \forall x\in ℂ\left(\left(A+x=0\wedge x+A=0\right)\to A+x=0\right)$$
8		sn-negex12	$$⊢A\in ℂ\to \exists x\in ℂ\left(A+x=0\wedge x+A=0\right)$$
9	1 8	syl	$$⊢\phi \to \exists x\in ℂ\left(A+x=0\wedge x+A=0\right)$$
10		0cn	$$⊢0\in ℂ$$
11		sn-subeu	$$⊢\left(A\in ℂ\wedge 0\in ℂ\right)\to \exists !x\in ℂA+x=0$$
12	1 10 11	sylancl	$$⊢\phi \to \exists !x\in ℂA+x=0$$
13		riotass2	$$⊢\left(\left(ℂ\subseteq ℂ\wedge \forall x\in ℂ\left(\left(A+x=0\wedge x+A=0\right)\to A+x=0\right)\right)\wedge \left(\exists x\in ℂ\left(A+x=0\wedge x+A=0\right)\wedge \exists !x\in ℂA+x=0\right)\right)\to \left(\iota x\in ℂ|\left(A+x=0\wedge x+A=0\right)\right)=\left(\iota x\in ℂ|A+x=0\right)$$
14	4 7 9 12 13	syl22anc	$$⊢\phi \to \left(\iota x\in ℂ|\left(A+x=0\wedge x+A=0\right)\right)=\left(\iota x\in ℂ|A+x=0\right)$$
15		oveq2	$$⊢x=B\to A+x=A+B$$
16	15	eqeq1d	$$⊢x=B\to \left(A+x=0\leftrightarrow A+B=0\right)$$
17	16	riota2	$$⊢\left(B\in ℂ\wedge \exists !x\in ℂA+x=0\right)\to \left(A+B=0\leftrightarrow \left(\iota x\in ℂ|A+x=0\right)=B\right)$$
18	2 12 17	syl2anc	$$⊢\phi \to \left(A+B=0\leftrightarrow \left(\iota x\in ℂ|A+x=0\right)=B\right)$$
19	3 18	mpbid	$$⊢\phi \to \left(\iota x\in ℂ|A+x=0\right)=B$$
20	14 19	eqtrd	$$⊢\phi \to \left(\iota x\in ℂ|\left(A+x=0\wedge x+A=0\right)\right)=B$$
21		reurmo	$$⊢\exists !x\in ℂA+x=0\to {\exists }^{*}x\in ℂA+x=0$$
22	5	rmoimi	$$⊢{\exists }^{*}x\in ℂA+x=0\to {\exists }^{*}x\in ℂ\left(A+x=0\wedge x+A=0\right)$$
23	12 21 22	3syl	$$⊢\phi \to {\exists }^{*}x\in ℂ\left(A+x=0\wedge x+A=0\right)$$
24		reu5	$$⊢\exists !x\in ℂ\left(A+x=0\wedge x+A=0\right)\leftrightarrow \left(\exists x\in ℂ\left(A+x=0\wedge x+A=0\right)\wedge {\exists }^{*}x\in ℂ\left(A+x=0\wedge x+A=0\right)\right)$$
25	9 23 24	sylanbrc	$$⊢\phi \to \exists !x\in ℂ\left(A+x=0\wedge x+A=0\right)$$
26		oveq1	$$⊢x=B\to x+A=B+A$$
27	26	eqeq1d	$$⊢x=B\to \left(x+A=0\leftrightarrow B+A=0\right)$$
28	16 27	anbi12d	$$⊢x=B\to \left(\left(A+x=0\wedge x+A=0\right)\leftrightarrow \left(A+B=0\wedge B+A=0\right)\right)$$
29	28	riota2	$$⊢\left(B\in ℂ\wedge \exists !x\in ℂ\left(A+x=0\wedge x+A=0\right)\right)\to \left(\left(A+B=0\wedge B+A=0\right)\leftrightarrow \left(\iota x\in ℂ|\left(A+x=0\wedge x+A=0\right)\right)=B\right)$$
30	2 25 29	syl2anc	$$⊢\phi \to \left(\left(A+B=0\wedge B+A=0\right)\leftrightarrow \left(\iota x\in ℂ|\left(A+x=0\wedge x+A=0\right)\right)=B\right)$$
31	20 30	mpbird	$$⊢\phi \to \left(A+B=0\wedge B+A=0\right)$$
32	31	simprd	$$⊢\phi \to B+A=0$$