Theorem angmgm

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

	Ref	Expression
Hypotheses	angmgmval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	angmgmval.a	⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
	angmgmval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	angmgmval.d	⊢ − = ( dist ‘ 𝐺 )
	angmgmval.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
	angmgmval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	angmgmval.o	⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
	angmgmval.j	⊢ 𝐽 = ( AngMgm ‘ 𝐺 )
	angmgm.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	angmgm.1	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
Assertion	angmgm	⊢ ( 𝜑 → 𝐽 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		angmgmval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		angmgmval.a	⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3		angmgmval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		angmgmval.d	⊢ − = ( dist ‘ 𝐺 )
5		angmgmval.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
6		angmgmval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
7		angmgmval.o	⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
8		angmgmval.j	⊢ 𝐽 = ( AngMgm ‘ 𝐺 )
9		angmgm.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
10		angmgm.1	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
11	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝐺 ∈ TarskiG )
12		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝑃 )
13		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝑃 )
14		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
15	14	necomd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ≠ 𝑥 )
16	13 15	eldifsnd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) )
17	1 2 3 4 5 6 7 8 11 12 16	angmgmlem	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑥 𝑦 𝑥 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) ) )
18	17	simpld	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → 𝐽 ∈ Mgm )
19	1 4 3 9 10	tglowdim1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑥 ≠ 𝑦 )
20	18 19	r19.29vva	⊢ ( 𝜑 → 𝐽 ∈ Mgm )