Metamath Proof Explorer

Theorem angmgmbas

Description: The base set of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses angmgmbas.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
angmgmbas.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
angmgmbas.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
angmgmbas.j ⊢ 𝐽 = ( AngMgm ‘ 𝐺 )
angmgmbas.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
Assertion angmgmbas ( 𝜑 → ( 𝐴 / ∼ ) = ( Base ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 angmgmbas.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmgmbas.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmgmbas.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
4 angmgmbas.j ⊢ 𝐽 = ( AngMgm ‘ 𝐺 )
5 angmgmbas.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
7 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
8 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
9 eqid ⊢ ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
10 eqid ⊢ ( ≤∠ ‘ 𝐺 ) = ( ≤∠ ‘ 𝐺 )
11 1 2 6 7 3 8 9 4 10 angmgmval ⊢ ( 𝐺 ∈ TarskiG → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } /s ∼ ) )
12 5 11 syl ⊢ ( 𝜑 → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } /s ∼ ) )
13 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
14 2 13 rabex2 ⊢ 𝐴 ∈ V
15 1nn ⊢ 1 ∈ ℕ
16 basendx ⊢ ( Base ‘ ndx ) = 1
17 1lt2 ⊢ 1 < 2
18 2nn ⊢ 2 ∈ ℕ
19 plusgndx ⊢ ( +g ‘ ndx ) = 2
20 2lt10 ⊢ 2 < 1 0
21 10nn ⊢ 1 0 ∈ ℕ
22 plendx ⊢ ( le ‘ ndx ) = 1 0
23 15 16 17 18 19 20 21 22 strle3 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } Struct ⟨ 1 , 1 0 ⟩
24 baseid ⊢ Base = Slot ( Base ‘ ndx )
25 snsstp1 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ }
26 23 24 25 strfv ⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ) )
27 14 26 mp1i ⊢ ( 𝜑 → 𝐴 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ) )
28 3 fvexi ⊢ ∼ ∈ V
29 28 a1i ⊢ ( 𝜑 → ∼ ∈ V )
30 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ∈ V
31 30 a1i ⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝐺 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝐺 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝐺 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝐺 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ∈ V )
32 12 27 29 31 qusbas ⊢ ( 𝜑 → ( 𝐴 / ∼ ) = ( Base ‘ 𝐽 ) )