Theorem cyccom

Description: Condition for an operation to be commutative. Lemma for cycsubmcom and cygabl . Formerly part of proof for cygabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 20-Jan-2024)

	Ref	Expression
Hypotheses	cyccom.c	$$⊢\phi \to \forall c\in C\exists x\in Zc=x\underset{\dot{}}{·}A$$
	cyccom.d	$$⊢\phi \to \forall m\in Z\forall n\in Z\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)$$
	cyccom.x	$$⊢\phi \to X\in C$$
	cyccom.y	$$⊢\phi \to Y\in C$$
	cyccom.z	$$⊢\phi \to Z\subseteq ℂ$$
Assertion	cyccom	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		cyccom.c	$$⊢\phi \to \forall c\in C\exists x\in Zc=x\underset{\dot{}}{·}A$$
2		cyccom.d	$$⊢\phi \to \forall m\in Z\forall n\in Z\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)$$
3		cyccom.x	$$⊢\phi \to X\in C$$
4		cyccom.y	$$⊢\phi \to Y\in C$$
5		cyccom.z	$$⊢\phi \to Z\subseteq ℂ$$
6		eqeq1	$$⊢c=Y\to \left(c=x\underset{\dot{}}{·}A\leftrightarrow Y=x\underset{\dot{}}{·}A\right)$$
7	6	rexbidv	$$⊢c=Y\to \left(\exists x\in Zc=x\underset{\dot{}}{·}A\leftrightarrow \exists x\in ZY=x\underset{\dot{}}{·}A\right)$$
8	7	rspccv	$$⊢\forall c\in C\exists x\in Zc=x\underset{\dot{}}{·}A\to \left(Y\in C\to \exists x\in ZY=x\underset{\dot{}}{·}A\right)$$
9	1 8	syl	$$⊢\phi \to \left(Y\in C\to \exists x\in ZY=x\underset{\dot{}}{·}A\right)$$
10		eqeq1	$$⊢c=X\to \left(c=x\underset{\dot{}}{·}A\leftrightarrow X=x\underset{\dot{}}{·}A\right)$$
11	10	rexbidv	$$⊢c=X\to \left(\exists x\in Zc=x\underset{\dot{}}{·}A\leftrightarrow \exists x\in ZX=x\underset{\dot{}}{·}A\right)$$
12	11	rspccv	$$⊢\forall c\in C\exists x\in Zc=x\underset{\dot{}}{·}A\to \left(X\in C\to \exists x\in ZX=x\underset{\dot{}}{·}A\right)$$
13	1 12	syl	$$⊢\phi \to \left(X\in C\to \exists x\in ZX=x\underset{\dot{}}{·}A\right)$$
14		oveq1	$$⊢x=y\to x\underset{\dot{}}{·}A=y\underset{\dot{}}{·}A$$
15	14	eqeq2d	$$⊢x=y\to \left(Y=x\underset{\dot{}}{·}A\leftrightarrow Y=y\underset{\dot{}}{·}A\right)$$
16	15	cbvrexvw	$$⊢\exists x\in ZY=x\underset{\dot{}}{·}A\leftrightarrow \exists y\in ZY=y\underset{\dot{}}{·}A$$
17		reeanv	$$⊢\exists x\in Z\exists y\in Z\left(X=x\underset{\dot{}}{·}A\wedge Y=y\underset{\dot{}}{·}A\right)\leftrightarrow \left(\exists x\in ZX=x\underset{\dot{}}{·}A\wedge \exists y\in ZY=y\underset{\dot{}}{·}A\right)$$
18	5	sseld	$$⊢\phi \to \left(x\in Z\to x\in ℂ\right)$$
19	18	com12	$$⊢x\in Z\to \left(\phi \to x\in ℂ\right)$$
20	19	adantr	$$⊢\left(x\in Z\wedge y\in Z\right)\to \left(\phi \to x\in ℂ\right)$$
21	20	impcom	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to x\in ℂ$$
22	5	sseld	$$⊢\phi \to \left(y\in Z\to y\in ℂ\right)$$
23	22	a1d	$$⊢\phi \to \left(x\in Z\to \left(y\in Z\to y\in ℂ\right)\right)$$
24	23	imp32	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to y\in ℂ$$
25	21 24	addcomd	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to x+y=y+x$$
26	25	oveq1d	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(x+y\right)\underset{\dot{}}{·}A=\left(y+x\right)\underset{\dot{}}{·}A$$
27		simpr	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(x\in Z\wedge y\in Z\right)$$
28	2	adantr	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \forall m\in Z\forall n\in Z\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)$$
29		oveq1	$$⊢m=x\to m+n=x+n$$
30	29	oveq1d	$$⊢m=x\to \left(m+n\right)\underset{\dot{}}{·}A=\left(x+n\right)\underset{\dot{}}{·}A$$
31		oveq1	$$⊢m=x\to m\underset{\dot{}}{·}A=x\underset{\dot{}}{·}A$$
32	31	oveq1d	$$⊢m=x\to \left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)$$
33	30 32	eqeq12d	$$⊢m=x\to \left(\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\leftrightarrow \left(x+n\right)\underset{\dot{}}{·}A=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\right)$$
34		oveq2	$$⊢n=y\to x+n=x+y$$
35	34	oveq1d	$$⊢n=y\to \left(x+n\right)\underset{\dot{}}{·}A=\left(x+y\right)\underset{\dot{}}{·}A$$
36		oveq1	$$⊢n=y\to n\underset{\dot{}}{·}A=y\underset{\dot{}}{·}A$$
37	36	oveq2d	$$⊢n=y\to \left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)$$
38	35 37	eqeq12d	$$⊢n=y\to \left(\left(x+n\right)\underset{\dot{}}{·}A=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\leftrightarrow \left(x+y\right)\underset{\dot{}}{·}A=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)\right)$$
39	33 38	rspc2va	$$⊢\left(\left(x\in Z\wedge y\in Z\right)\wedge \forall m\in Z\forall n\in Z\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\right)\to \left(x+y\right)\underset{\dot{}}{·}A=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)$$
40	27 28 39	syl2anc	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(x+y\right)\underset{\dot{}}{·}A=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)$$
41	27	ancomd	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(y\in Z\wedge x\in Z\right)$$
42		oveq1	$$⊢m=y\to m+n=y+n$$
43	42	oveq1d	$$⊢m=y\to \left(m+n\right)\underset{\dot{}}{·}A=\left(y+n\right)\underset{\dot{}}{·}A$$
44		oveq1	$$⊢m=y\to m\underset{\dot{}}{·}A=y\underset{\dot{}}{·}A$$
45	44	oveq1d	$$⊢m=y\to \left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)$$
46	43 45	eqeq12d	$$⊢m=y\to \left(\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\leftrightarrow \left(y+n\right)\underset{\dot{}}{·}A=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\right)$$
47		oveq2	$$⊢n=x\to y+n=y+x$$
48	47	oveq1d	$$⊢n=x\to \left(y+n\right)\underset{\dot{}}{·}A=\left(y+x\right)\underset{\dot{}}{·}A$$
49		oveq1	$$⊢n=x\to n\underset{\dot{}}{·}A=x\underset{\dot{}}{·}A$$
50	49	oveq2d	$$⊢n=x\to \left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)$$
51	48 50	eqeq12d	$$⊢n=x\to \left(\left(y+n\right)\underset{\dot{}}{·}A=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\leftrightarrow \left(y+x\right)\underset{\dot{}}{·}A=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)\right)$$
52	46 51	rspc2va	$$⊢\left(\left(y\in Z\wedge x\in Z\right)\wedge \forall m\in Z\forall n\in Z\left(m+n\right)\underset{\dot{}}{·}A=\left(m\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(n\underset{\dot{}}{·}A\right)\right)\to \left(y+x\right)\underset{\dot{}}{·}A=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)$$
53	41 28 52	syl2anc	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(y+x\right)\underset{\dot{}}{·}A=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)$$
54	26 40 53	3eqtr3d	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)$$
55		oveq12	$$⊢\left(X=x\underset{\dot{}}{·}A\wedge Y=y\underset{\dot{}}{·}A\right)\to X\underset{\dot{}}{+}Y=\left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)$$
56		oveq12	$$⊢\left(Y=y\underset{\dot{}}{·}A\wedge X=x\underset{\dot{}}{·}A\right)\to Y\underset{\dot{}}{+}X=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)$$
57	56	ancoms	$$⊢\left(X=x\underset{\dot{}}{·}A\wedge Y=y\underset{\dot{}}{·}A\right)\to Y\underset{\dot{}}{+}X=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)$$
58	55 57	eqeq12d	$$⊢\left(X=x\underset{\dot{}}{·}A\wedge Y=y\underset{\dot{}}{·}A\right)\to \left(X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\leftrightarrow \left(x\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}A\right)=\left(y\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}A\right)\right)$$
59	54 58	syl5ibrcom	$$⊢\left(\phi \wedge \left(x\in Z\wedge y\in Z\right)\right)\to \left(\left(X=x\underset{\dot{}}{·}A\wedge Y=y\underset{\dot{}}{·}A\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
60	59	rexlimdvva	$$⊢\phi \to \left(\exists x\in Z\exists y\in Z\left(X=x\underset{\dot{}}{·}A\wedge Y=y\underset{\dot{}}{·}A\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
61	17 60	biimtrrid	$$⊢\phi \to \left(\left(\exists x\in ZX=x\underset{\dot{}}{·}A\wedge \exists y\in ZY=y\underset{\dot{}}{·}A\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
62	61	expd	$$⊢\phi \to \left(\exists x\in ZX=x\underset{\dot{}}{·}A\to \left(\exists y\in ZY=y\underset{\dot{}}{·}A\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$
63	16 62	syl7bi	$$⊢\phi \to \left(\exists x\in ZX=x\underset{\dot{}}{·}A\to \left(\exists x\in ZY=x\underset{\dot{}}{·}A\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$
64	13 63	syld	$$⊢\phi \to \left(X\in C\to \left(\exists x\in ZY=x\underset{\dot{}}{·}A\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$
65	64	com23	$$⊢\phi \to \left(\exists x\in ZY=x\underset{\dot{}}{·}A\to \left(X\in C\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$
66	9 65	syld	$$⊢\phi \to \left(Y\in C\to \left(X\in C\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$
67	4 3 66	mp2d	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$