Theorem sn-00idlem1

Description: Lemma for sn-00id . (Contributed by SN, 25-Dec-2023)

	Ref	Expression
Assertion	sn-00idlem1	|- ( A e. RR -> ( A x. ( 0 -R 0 ) ) = ( A -R A ) )

Proof

Step	Hyp	Ref	Expression
1		1re	|- 1 e. RR
2		resubdi	|- ( ( A e. RR /\ 1 e. RR /\ 1 e. RR ) -> ( A x. ( 1 -R 1 ) ) = ( ( A x. 1 ) -R ( A x. 1 ) ) )
3	1 1 2	mp3an23	|- ( A e. RR -> ( A x. ( 1 -R 1 ) ) = ( ( A x. 1 ) -R ( A x. 1 ) ) )
4		re1m1e0m0	|- ( 1 -R 1 ) = ( 0 -R 0 )
5	4	oveq2i	|- ( A x. ( 1 -R 1 ) ) = ( A x. ( 0 -R 0 ) )
6	5	a1i	|- ( A e. RR -> ( A x. ( 1 -R 1 ) ) = ( A x. ( 0 -R 0 ) ) )
7		ax-1rid	|- ( A e. RR -> ( A x. 1 ) = A )
8	7 7	oveq12d	|- ( A e. RR -> ( ( A x. 1 ) -R ( A x. 1 ) ) = ( A -R A ) )
9	3 6 8	3eqtr3d	|- ( A e. RR -> ( A x. ( 0 -R 0 ) ) = ( A -R A ) )