Theorem rglcom4d

Description: Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom depends on the closure of the addition, the (left and right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025)

	Ref	Expression
Hypotheses	o2timesd.e	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
	o2timesd.u	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
	o2timesd.i	$$⊢\phi \to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
	o2timesd.x	$$⊢\phi \to X\in B$$
	rglcom4d.a	$$⊢\phi \to \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y\in B$$
	rglcom4d.d	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
	rglcom4d.y	$$⊢\phi \to Y\in B$$
Assertion	rglcom4d	$$⊢\phi \to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Y\right)=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		o2timesd.e	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
2		o2timesd.u	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
3		o2timesd.i	$$⊢\phi \to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
4		o2timesd.x	$$⊢\phi \to X\in B$$
5		rglcom4d.a	$$⊢\phi \to \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y\in B$$
6		rglcom4d.d	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
7		rglcom4d.y	$$⊢\phi \to Y\in B$$
8	2 2	jca	$$⊢\phi \to \left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\right)$$
9		oveq1	$$⊢x=\underset{\dot{}}{1}\to x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\underset{\dot{}}{+}y$$
10	9	eleq1d	$$⊢x=\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{+}y\in B\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{+}y\in B\right)$$
11		oveq2	$$⊢y=\underset{\dot{}}{1}\to \underset{\dot{}}{1}\underset{\dot{}}{+}y=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}$$
12	11	eleq1d	$$⊢y=\underset{\dot{}}{1}\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\in B\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\in B\right)$$
13	10 12	rspc2v	$$⊢\left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\right)\to \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y\in B\to \underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\in B\right)$$
14	8 5 13	sylc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\in B$$
15	14 4 7	3jca	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\in B\wedge X\in B\wedge Y\in B\right)$$
16		oveq1	$$⊢x=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)$$
17		oveq1	$$⊢x=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\to x\underset{\dot{}}{·}y=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}y$$
18		oveq1	$$⊢x=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\to x\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z$$
19	17 18	oveq12d	$$⊢x=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)$$
20	16 19	eqeq12d	$$⊢x=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)\right)$$
21		oveq1	$$⊢y=X\to y\underset{\dot{}}{+}z=X\underset{\dot{}}{+}z$$
22	21	oveq2d	$$⊢y=X\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}z\right)$$
23		oveq2	$$⊢y=X\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}y=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X$$
24	23	oveq1d	$$⊢y=X\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)$$
25	22 24	eqeq12d	$$⊢y=X\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)\right)$$
26		oveq2	$$⊢z=Y\to X\underset{\dot{}}{+}z=X\underset{\dot{}}{+}Y$$
27	26	oveq2d	$$⊢z=Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)$$
28		oveq2	$$⊢z=Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y$$
29	28	oveq2d	$$⊢z=Y\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y\right)$$
30	27 29	eqeq12d	$$⊢z=Y\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}z\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y\right)\right)$$
31	20 25 30	rspc3v	$$⊢\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\in B\wedge X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y\right)\right)$$
32	15 6 31	sylc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y\right)$$
33		oveq1	$$⊢x=X\to x\underset{\dot{}}{+}y=X\underset{\dot{}}{+}y$$
34	33	eleq1d	$$⊢x=X\to \left(x\underset{\dot{}}{+}y\in B\leftrightarrow X\underset{\dot{}}{+}y\in B\right)$$
35		oveq2	$$⊢y=Y\to X\underset{\dot{}}{+}y=X\underset{\dot{}}{+}Y$$
36	35	eleq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{+}y\in B\leftrightarrow X\underset{\dot{}}{+}Y\in B\right)$$
37	34 36	rspc2va	$$⊢\left(\left(X\in B\wedge Y\in B\right)\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
38	4 7 5 37	syl21anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$
39	2 2 38	3jca	$$⊢\phi \to \left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\wedge X\underset{\dot{}}{+}Y\in B\right)$$
40	9	oveq1d	$$⊢x=\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z$$
41		oveq1	$$⊢x=\underset{\dot{}}{1}\to x\underset{\dot{}}{·}z=\underset{\dot{}}{1}\underset{\dot{}}{·}z$$
42	41	oveq1d	$$⊢x=\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
43	40 42	eqeq12d	$$⊢x=\underset{\dot{}}{1}\to \left(\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)$$
44	11	oveq1d	$$⊢y=\underset{\dot{}}{1}\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z$$
45		oveq1	$$⊢y=\underset{\dot{}}{1}\to y\underset{\dot{}}{·}z=\underset{\dot{}}{1}\underset{\dot{}}{·}z$$
46	45	oveq2d	$$⊢y=\underset{\dot{}}{1}\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)$$
47	44 46	eqeq12d	$$⊢y=\underset{\dot{}}{1}\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\right)$$
48		oveq2	$$⊢z=X\underset{\dot{}}{+}Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)$$
49		oveq2	$$⊢z=X\underset{\dot{}}{+}Y\to \underset{\dot{}}{1}\underset{\dot{}}{·}z=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)$$
50	49 49	oveq12d	$$⊢z=X\underset{\dot{}}{+}Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)$$
51	48 50	eqeq12d	$$⊢z=X\underset{\dot{}}{+}Y\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\right)$$
52	43 47 51	rspc3v	$$⊢\left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\wedge X\underset{\dot{}}{+}Y\in B\right)\to \left(\forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\right)$$
53	39 1 52	sylc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)$$
54	32 53	eqtr3d	$$⊢\phi \to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)$$
55	1 2 3 4	o2timesd	$$⊢\phi \to X\underset{\dot{}}{+}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X$$
56	55	eqcomd	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=X\underset{\dot{}}{+}X$$
57	1 2 3 7	o2timesd	$$⊢\phi \to Y\underset{\dot{}}{+}Y=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y$$
58	57	eqcomd	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y=Y\underset{\dot{}}{+}Y$$
59	56 58	oveq12d	$$⊢\phi \to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Y\right)=\left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Y\right)$$
60		oveq2	$$⊢x=X\underset{\dot{}}{+}Y\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)$$
61		id	$$⊢x=X\underset{\dot{}}{+}Y\to x=X\underset{\dot{}}{+}Y$$
62	60 61	eqeq12d	$$⊢x=X\underset{\dot{}}{+}Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}Y\right)$$
63	62	rspcva	$$⊢\left(X\underset{\dot{}}{+}Y\in B\wedge \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}Y$$
64	38 3 63	syl2anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=X\underset{\dot{}}{+}Y$$
65	64 64	oveq12d	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
66	54 59 65	3eqtr3d	$$⊢\phi \to \left(X\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Y\right)=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$