Theorem angmgm0g

Description: The identity element of the angle addition 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 ‘ 𝐺 )
	angmgmlem.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	angmgmlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	angmgmlem.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
Assertion	angmgm0g	⊢ ( 𝜑 → [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) )

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		angmgmlem.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
10		angmgmlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11		angmgmlem.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
12	1 2 3 4 5 6 7 8 9 10 11	angmgmlem	⊢ ( 𝜑 → ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) ) )
13	12	simprd	⊢ ( 𝜑 → [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) )