Theorem nmulcom

Description: Natural multiplication commutes. (Contributed by Scott Fenton, 10-Jun-2026)

	Ref	Expression
Assertion	nmulcom	|- ( ( A e. On /\ B e. On ) -> ( A .no B ) = ( B .no A ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( a = c -> ( a .no b ) = ( c .no b ) )
2		oveq2	|- ( a = c -> ( b .no a ) = ( b .no c ) )
3	1 2	eqeq12d	|- ( a = c -> ( ( a .no b ) = ( b .no a ) <-> ( c .no b ) = ( b .no c ) ) )
4		oveq2	|- ( b = d -> ( c .no b ) = ( c .no d ) )
5		oveq1	|- ( b = d -> ( b .no c ) = ( d .no c ) )
6	4 5	eqeq12d	|- ( b = d -> ( ( c .no b ) = ( b .no c ) <-> ( c .no d ) = ( d .no c ) ) )
7		oveq1	|- ( a = c -> ( a .no d ) = ( c .no d ) )
8		oveq2	|- ( a = c -> ( d .no a ) = ( d .no c ) )
9	7 8	eqeq12d	|- ( a = c -> ( ( a .no d ) = ( d .no a ) <-> ( c .no d ) = ( d .no c ) ) )
10		oveq1	|- ( a = A -> ( a .no b ) = ( A .no b ) )
11		oveq2	|- ( a = A -> ( b .no a ) = ( b .no A ) )
12	10 11	eqeq12d	|- ( a = A -> ( ( a .no b ) = ( b .no a ) <-> ( A .no b ) = ( b .no A ) ) )
13		oveq2	|- ( b = B -> ( A .no b ) = ( A .no B ) )
14		oveq1	|- ( b = B -> ( b .no A ) = ( B .no A ) )
15	13 14	eqeq12d	|- ( b = B -> ( ( A .no b ) = ( b .no A ) <-> ( A .no B ) = ( B .no A ) ) )
16		oveq1	|- ( c = z -> ( c .no b ) = ( z .no b ) )
17		oveq2	|- ( c = z -> ( b .no c ) = ( b .no z ) )
18	16 17	eqeq12d	|- ( c = z -> ( ( c .no b ) = ( b .no c ) <-> ( z .no b ) = ( b .no z ) ) )
19		simplr2	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. c e. a ( c .no b ) = ( b .no c ) )
20		simprl	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> z e. a )
21	18 19 20	rspcdva	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( z .no b ) = ( b .no z ) )
22		oveq2	|- ( d = y -> ( a .no d ) = ( a .no y ) )
23		oveq1	|- ( d = y -> ( d .no a ) = ( y .no a ) )
24	22 23	eqeq12d	|- ( d = y -> ( ( a .no d ) = ( d .no a ) <-> ( a .no y ) = ( y .no a ) ) )
25		simplr3	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. d e. b ( a .no d ) = ( d .no a ) )
26		simprr	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> y e. b )
27	24 25 26	rspcdva	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( a .no y ) = ( y .no a ) )
28	21 27	oveq12d	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( z .no b ) +no ( a .no y ) ) = ( ( b .no z ) +no ( y .no a ) ) )
29		simpllr	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> b e. On )
30		simplll	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> a e. On )
31		onelon	|- ( ( a e. On /\ z e. a ) -> z e. On )
32	30 20 31	syl2anc	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> z e. On )
33		nmulcl	|- ( ( b e. On /\ z e. On ) -> ( b .no z ) e. On )
34	29 32 33	syl2anc	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( b .no z ) e. On )
35		onelon	|- ( ( b e. On /\ y e. b ) -> y e. On )
36	29 26 35	syl2anc	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> y e. On )
37		nmulcl	|- ( ( y e. On /\ a e. On ) -> ( y .no a ) e. On )
38	36 30 37	syl2anc	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( y .no a ) e. On )
39		naddcom	|- ( ( ( b .no z ) e. On /\ ( y .no a ) e. On ) -> ( ( b .no z ) +no ( y .no a ) ) = ( ( y .no a ) +no ( b .no z ) ) )
40	34 38 39	syl2anc	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( b .no z ) +no ( y .no a ) ) = ( ( y .no a ) +no ( b .no z ) ) )
41	28 40	eqtrd	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( z .no b ) +no ( a .no y ) ) = ( ( y .no a ) +no ( b .no z ) ) )
42		oveq1	|- ( c = z -> ( c .no d ) = ( z .no d ) )
43		oveq2	|- ( c = z -> ( d .no c ) = ( d .no z ) )
44	42 43	eqeq12d	|- ( c = z -> ( ( c .no d ) = ( d .no c ) <-> ( z .no d ) = ( d .no z ) ) )
45		oveq2	|- ( d = y -> ( z .no d ) = ( z .no y ) )
46		oveq1	|- ( d = y -> ( d .no z ) = ( y .no z ) )
47	45 46	eqeq12d	|- ( d = y -> ( ( z .no d ) = ( d .no z ) <-> ( z .no y ) = ( y .no z ) ) )
48		simplr1	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. c e. a A. d e. b ( c .no d ) = ( d .no c ) )
49	44 47 48 20 26	rspc2dv	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( z .no y ) = ( y .no z ) )
50	49	oveq2d	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( x +no ( z .no y ) ) = ( x +no ( y .no z ) ) )
51	41 50	eleq12d	|- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) )
52	51	2ralbidva	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> A. z e. a A. y e. b ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) )
53		ralcom	|- ( A. z e. a A. y e. b ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) <-> A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) )
54	52 53	bitrdi	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) )
55	54	rabbidv	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } = { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } )
56	55	inteqd	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } )
57		nmulval	|- ( ( a e. On /\ b e. On ) -> ( a .no b ) = |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } )
58	57	adantr	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( a .no b ) = |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } )
59		nmulval	|- ( ( b e. On /\ a e. On ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } )
60	59	ancoms	|- ( ( a e. On /\ b e. On ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } )
61	60	adantr	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } )
62	56 58 61	3eqtr4d	|- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( a .no b ) = ( b .no a ) )
63	62	ex	|- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) -> ( a .no b ) = ( b .no a ) ) )
64	3 6 9 12 15 63	on2ind	|- ( ( A e. On /\ B e. On ) -> ( A .no B ) = ( B .no A ) )