Theorem bru3cj

Description: The complex conjugate of the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Hypothesis	bru3eq.w	|- W = ( bRoU ` 3 )
Assertion	bru3cj	|- ( * ` W ) = ( W ^ 2 )

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	|- W = ( bRoU ` 3 )
2		3nn	|- 3 e. NN
3		bruval2	|- ( 3 e. NN -> ( bRoU ` 3 ) = ( -u 1 ^c ( 2 / 3 ) ) )
4	2 3	ax-mp	|- ( bRoU ` 3 ) = ( -u 1 ^c ( 2 / 3 ) )
5	1 4	eqtri	|- W = ( -u 1 ^c ( 2 / 3 ) )
6	5	fveq2i	|- ( * ` W ) = ( * ` ( -u 1 ^c ( 2 / 3 ) ) )
7		neg1cn	|- -u 1 e. CC
8		2cn	|- 2 e. CC
9		3cn	|- 3 e. CC
10		3ne0	|- 3 =/= 0
11	8 9 10	divcli	|- ( 2 / 3 ) e. CC
12	7 11	pm3.2i	|- ( -u 1 e. CC /\ ( 2 / 3 ) e. CC )
13		cxpcl	|- ( ( -u 1 e. CC /\ ( 2 / 3 ) e. CC ) -> ( -u 1 ^c ( 2 / 3 ) ) e. CC )
14	12 13	ax-mp	|- ( -u 1 ^c ( 2 / 3 ) ) e. CC
15		exp1	|- ( ( -u 1 ^c ( 2 / 3 ) ) e. CC -> ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) = ( -u 1 ^c ( 2 / 3 ) ) )
16	14 15	ax-mp	|- ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) = ( -u 1 ^c ( 2 / 3 ) )
17	16	eqcomi	|- ( -u 1 ^c ( 2 / 3 ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 )
18	17	fveq2i	|- ( * ` ( -u 1 ^c ( 2 / 3 ) ) ) = ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) )
19		1z	|- 1 e. ZZ
20	2 19	pm3.2i	|- ( 3 e. NN /\ 1 e. ZZ )
21		root1cj	|- ( ( 3 e. NN /\ 1 e. ZZ ) -> ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) ) )
22	20 21	ax-mp	|- ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) )
23	18 22	eqtri	|- ( * ` ( -u 1 ^c ( 2 / 3 ) ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) )
24	5	eqcomi	|- ( -u 1 ^c ( 2 / 3 ) ) = W
25		3m1e2	|- ( 3 - 1 ) = 2
26	24 25	oveq12i	|- ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) ) = ( W ^ 2 )
27	6 23 26	3eqtri	|- ( * ` W ) = ( W ^ 2 )