Theorem angmgm

Description: The angle addition magma is a magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

	Ref	Expression
Hypotheses	angmgmval.p	|- P = ( Base ` G )
	angmgmval.a	|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
	angmgmval.i	|- I = ( Itv ` G )
	angmgmval.d	|- .- = ( dist ` G )
	angmgmval.c	|- .~ = ( cgrA ` G )
	angmgmval.l	|- L = ( LineG ` G )
	angmgmval.o	|- .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
	angmgmval.j	|- J = ( AngMgm ` G )
	angmgm.g	|- ( ph -> G e. TarskiG )
	angmgm.1	|- ( ph -> 2 <_ ( # ` P ) )
Assertion	angmgm	|- ( ph -> J e. Mgm )

Proof

Step	Hyp	Ref	Expression
1		angmgmval.p	|- P = ( Base ` G )
2		angmgmval.a	|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3		angmgmval.i	|- I = ( Itv ` G )
4		angmgmval.d	|- .- = ( dist ` G )
5		angmgmval.c	|- .~ = ( cgrA ` G )
6		angmgmval.l	|- L = ( LineG ` G )
7		angmgmval.o	|- .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
8		angmgmval.j	|- J = ( AngMgm ` G )
9		angmgm.g	|- ( ph -> G e. TarskiG )
10		angmgm.1	|- ( ph -> 2 <_ ( # ` P ) )
11	9	ad3antrrr	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> G e. TarskiG )
12		simpllr	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> x e. P )
13		simplr	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> y e. P )
14		simpr	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> x =/= y )
15	14	necomd	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> y =/= x )
16	13 15	eldifsnd	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> y e. ( P \ { x } ) )
17	1 2 3 4 5 6 7 8 11 12 16	angmgmlem	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> ( J e. Mgm /\ [ <" x y x "> ] .~ = ( 0g ` J ) ) )
18	17	simpld	|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ x =/= y ) -> J e. Mgm )
19	1 4 3 9 10	tglowdim1	|- ( ph -> E. x e. P E. y e. P x =/= y )
20	18 19	r19.29vva	|- ( ph -> J e. Mgm )