elcgrabasrd

Description: Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	elcgrabasrd.a	\|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) \| ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
	elcgrabasrd.p	\|- ( ph -> P e. V )
	elcgrabasrd.x	\|- ( ph -> X e. P )
	elcgrabasrd.y	\|- ( ph -> Y e. P )
	elcgrabasrd.z	\|- ( ph -> Z e. P )
	elcgrabasrd.1	\|- ( ph -> X =/= Y )
	elcgrabasrd.2	\|- ( ph -> Y =/= Z )
Assertion	elcgrabasrd	\|- ( ph -> <" X Y Z "> e. A )

Proof

Step	Hyp	Ref	Expression
1		elcgrabasrd.a	\|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) \| ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
2		elcgrabasrd.p	\|- ( ph -> P e. V )
3		elcgrabasrd.x	\|- ( ph -> X e. P )
4		elcgrabasrd.y	\|- ( ph -> Y e. P )
5		elcgrabasrd.z	\|- ( ph -> Z e. P )
6		elcgrabasrd.1	\|- ( ph -> X =/= Y )
7		elcgrabasrd.2	\|- ( ph -> Y =/= Z )
8		fveq1	\|- ( d = <" X Y Z "> -> ( d ` 0 ) = ( <" X Y Z "> ` 0 ) )
9		fveq1	\|- ( d = <" X Y Z "> -> ( d ` 1 ) = ( <" X Y Z "> ` 1 ) )
10	8 9	neeq12d	\|- ( d = <" X Y Z "> -> ( ( d ` 0 ) =/= ( d ` 1 ) <-> ( <" X Y Z "> ` 0 ) =/= ( <" X Y Z "> ` 1 ) ) )
11		fveq1	\|- ( d = <" X Y Z "> -> ( d ` 2 ) = ( <" X Y Z "> ` 2 ) )
12	9 11	neeq12d	\|- ( d = <" X Y Z "> -> ( ( d ` 1 ) =/= ( d ` 2 ) <-> ( <" X Y Z "> ` 1 ) =/= ( <" X Y Z "> ` 2 ) ) )
13	10 12	anbi12d	\|- ( d = <" X Y Z "> -> ( ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) <-> ( ( <" X Y Z "> ` 0 ) =/= ( <" X Y Z "> ` 1 ) /\ ( <" X Y Z "> ` 1 ) =/= ( <" X Y Z "> ` 2 ) ) ) )
14	2 3 4 5	s3rexrd	\|- ( ph -> <" X Y Z "> e. ( P ^m ( 0 ..^ 3 ) ) )
15		s3fv0	\|- ( X e. P -> ( <" X Y Z "> ` 0 ) = X )
16	3 15	syl	\|- ( ph -> ( <" X Y Z "> ` 0 ) = X )
17		s3fv1	\|- ( Y e. P -> ( <" X Y Z "> ` 1 ) = Y )
18	4 17	syl	\|- ( ph -> ( <" X Y Z "> ` 1 ) = Y )
19	6 16 18	3netr4d	\|- ( ph -> ( <" X Y Z "> ` 0 ) =/= ( <" X Y Z "> ` 1 ) )
20		s3fv2	\|- ( Z e. P -> ( <" X Y Z "> ` 2 ) = Z )
21	5 20	syl	\|- ( ph -> ( <" X Y Z "> ` 2 ) = Z )
22	7 18 21	3netr4d	\|- ( ph -> ( <" X Y Z "> ` 1 ) =/= ( <" X Y Z "> ` 2 ) )
23	19 22	jca	\|- ( ph -> ( ( <" X Y Z "> ` 0 ) =/= ( <" X Y Z "> ` 1 ) /\ ( <" X Y Z "> ` 1 ) =/= ( <" X Y Z "> ` 2 ) ) )
24	13 14 23	elrabd	\|- ( ph -> <" X Y Z "> e. { d e. ( P ^m ( 0 ..^ 3 ) ) \| ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } )
25	24 1	eleqtrrdi	\|- ( ph -> <" X Y Z "> e. A )

Metamath Proof Explorer

Theorem elcgrabasrd

Proof