Theorem mulgass2

Description: An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	mulgass2.b	$$⊢B={\mathrm{Base}}_R$$
	mulgass2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mulgass2.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
Assertion	mulgass2	$$⊢\left(R\in \mathrm{Ring}\wedge \left(N\in \mathbb{Z}\wedge X\in B\wedge Y\in B\right)\right)\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgass2.b	$$⊢B={\mathrm{Base}}_R$$
2		mulgass2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		mulgass2.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
4		oveq1	$$⊢x=0\to x\underset{\dot{}}{·}X=0\underset{\dot{}}{·}X$$
5	4	oveq1d	$$⊢x=0\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
6		oveq1	$$⊢x=0\to x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=0\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
7	5 6	eqeq12d	$$⊢x=0\to \left(\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow \left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=0\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
8		oveq1	$$⊢x=y\to x\underset{\dot{}}{·}X=y\underset{\dot{}}{·}X$$
9	8	oveq1d	$$⊢x=y\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
10		oveq1	$$⊢x=y\to x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
11	9 10	eqeq12d	$$⊢x=y\to \left(\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow \left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
12		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{·}X=\left(y+1\right)\underset{\dot{}}{·}X$$
13	12	oveq1d	$$⊢x=y+1\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
14		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=\left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
15	13 14	eqeq12d	$$⊢x=y+1\to \left(\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow \left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
16		oveq1	$$⊢x=-y\to x\underset{\dot{}}{·}X=\left(-y\right)\underset{\dot{}}{·}X$$
17	16	oveq1d	$$⊢x=-y\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
18		oveq1	$$⊢x=-y\to x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=\left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
19	17 18	eqeq12d	$$⊢x=-y\to \left(\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow \left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
20		oveq1	$$⊢x=N\to x\underset{\dot{}}{·}X=N\underset{\dot{}}{·}X$$
21	20	oveq1d	$$⊢x=N\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
22		oveq1	$$⊢x=N\to x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
23	21 22	eqeq12d	$$⊢x=N\to \left(\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=x\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
24		eqid	$$⊢0_R=0_R$$
25	1 3 24	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to 0_R\underset{\dot{}}{\times }Y=0_R$$
26	25	3adant3	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to 0_R\underset{\dot{}}{\times }Y=0_R$$
27		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to X\in B$$
28	1 24 2	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{·}X=0_R$$
29	27 28	syl	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to 0\underset{\dot{}}{·}X=0_R$$
30	29	oveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to \left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=0_R\underset{\dot{}}{\times }Y$$
31	1 3	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\times }Y\in B$$
32	31	3com23	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to X\underset{\dot{}}{\times }Y\in B$$
33	1 24 2	mulg0	$$⊢X\underset{\dot{}}{\times }Y\in B\to 0\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=0_R$$
34	32 33	syl	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to 0\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=0_R$$
35	26 30 34	3eqtr4d	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to \left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=0\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
36		oveq1	$$⊢\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\to \left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)=\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)$$
37		simpl1	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to R\in \mathrm{Ring}$$
38		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
39	37 38	syl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to R\in \mathrm{Grp}$$
40		nn0z	$$⊢y\in {\mathbb{N}}_0\to y\in \mathbb{Z}$$
41	40	adantl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to y\in \mathbb{Z}$$
42	27	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to X\in B$$
43		eqid	$$⊢{+}_R={+}_R$$
44	1 2 43	mulgp1	$$⊢\left(R\in \mathrm{Grp}\wedge y\in \mathbb{Z}\wedge X\in B\right)\to \left(y+1\right)\underset{\dot{}}{·}X=\left(y\underset{\dot{}}{·}X\right){+}_{R}X$$
45	39 41 42 44	syl3anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(y+1\right)\underset{\dot{}}{·}X=\left(y\underset{\dot{}}{·}X\right){+}_{R}X$$
46	45	oveq1d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(\left(y\underset{\dot{}}{·}X\right){+}_{R}X\right)\underset{\dot{}}{\times }Y$$
47	38	3ad2ant1	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to R\in \mathrm{Grp}$$
48	47	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to R\in \mathrm{Grp}$$
49	1 2	mulgcl	$$⊢\left(R\in \mathrm{Grp}\wedge y\in \mathbb{Z}\wedge X\in B\right)\to y\underset{\dot{}}{·}X\in B$$
50	48 41 42 49	syl3anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to y\underset{\dot{}}{·}X\in B$$
51		simpl2	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to Y\in B$$
52	1 43 3	ringdir	$$⊢\left(R\in \mathrm{Ring}\wedge \left(y\underset{\dot{}}{·}X\in B\wedge X\in B\wedge Y\in B\right)\right)\to \left(\left(y\underset{\dot{}}{·}X\right){+}_{R}X\right)\underset{\dot{}}{\times }Y=\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)$$
53	37 50 42 51 52	syl13anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y\underset{\dot{}}{·}X\right){+}_{R}X\right)\underset{\dot{}}{\times }Y=\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)$$
54	46 53	eqtrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)$$
55	32	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to X\underset{\dot{}}{\times }Y\in B$$
56	1 2 43	mulgp1	$$⊢\left(R\in \mathrm{Grp}\wedge y\in \mathbb{Z}\wedge X\underset{\dot{}}{\times }Y\in B\right)\to \left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)$$
57	39 41 55 56	syl3anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)=\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)$$
58	54 57	eqeq12d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(\left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow \left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)=\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right){+}_R\left(X\underset{\dot{}}{\times }Y\right)\right)$$
59	36 58	syl5ibr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\to \left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
60	59	ex	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to \left(y\in {\mathbb{N}}_0\to \left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\to \left(\left(y+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(y+1\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)$$
61		fveq2	$$⊢\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\to {inv}_g\left(R\right)\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right)={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
62	47	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to R\in \mathrm{Grp}$$
63		nnz	$$⊢y\in \mathbb{N}\to y\in \mathbb{Z}$$
64	63	adantl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to y\in \mathbb{Z}$$
65	27	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to X\in B$$
66		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
67	1 2 66	mulgneg	$$⊢\left(R\in \mathrm{Grp}\wedge y\in \mathbb{Z}\wedge X\in B\right)\to \left(-y\right)\underset{\dot{}}{·}X={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}X\right)$$
68	62 64 65 67	syl3anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to \left(-y\right)\underset{\dot{}}{·}X={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}X\right)$$
69	68	oveq1d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to \left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
70		simpl1	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to R\in \mathrm{Ring}$$
71	62 64 65 49	syl3anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to y\underset{\dot{}}{·}X\in B$$
72		simpl2	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to Y\in B$$
73	1 3 66 70 71 72	ringmneg1	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to {inv}_g\left(R\right)\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y={inv}_g\left(R\right)\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right)$$
74	69 73	eqtrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to \left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y={inv}_g\left(R\right)\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right)$$
75	32	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to X\underset{\dot{}}{\times }Y\in B$$
76	1 2 66	mulgneg	$$⊢\left(R\in \mathrm{Grp}\wedge y\in \mathbb{Z}\wedge X\underset{\dot{}}{\times }Y\in B\right)\to \left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
77	62 64 75 76	syl3anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to \left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
78	74 77	eqeq12d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to \left(\left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\leftrightarrow {inv}_g\left(R\right)\left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y\right)={inv}_g\left(R\right)\left(y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)$$
79	61 78	syl5ibr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\wedge y\in \mathbb{N}\right)\to \left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\to \left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
80	79	ex	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to \left(y\in \mathbb{N}\to \left(\left(y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=y\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\to \left(\left(-y\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=\left(-y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)$$
81	7 11 15 19 23 35 60 80	zindd	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge X\in B\right)\to \left(N\in \mathbb{Z}\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
82	81	3exp	$$⊢R\in \mathrm{Ring}\to \left(Y\in B\to \left(X\in B\to \left(N\in \mathbb{Z}\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)\right)$$
83	82	com24	$$⊢R\in \mathrm{Ring}\to \left(N\in \mathbb{Z}\to \left(X\in B\to \left(Y\in B\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)\right)$$
84	83	3imp2	$$⊢\left(R\in \mathrm{Ring}\wedge \left(N\in \mathbb{Z}\wedge X\in B\wedge Y\in B\right)\right)\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=N\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$