angmgmbas

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

	Ref	Expression
Hypotheses	angmgmbas.p	$⊢ P = {Base}_{G}$
	angmgmbas.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmgmbas.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmgmbas.j	No typesetting found for \|- J = ( AngMgm ` G ) with typecode \|-
	angmgmbas.g	$⊢ φ \to G \in 𝒢_{Tarski}$
Assertion	angmgmbas	$⊢ φ \to A / \underset{˙}{\sim} = {Base}_{J}$

Proof

Step	Hyp	Ref	Expression
1		angmgmbas.p	$⊢ P = {Base}_{G}$
2		angmgmbas.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmgmbas.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
4		angmgmbas.j	Could not format J = ( AngMgm ` G ) : No typesetting found for \|- J = ( AngMgm ` G ) with typecode \|-
5		angmgmbas.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		eqid	$⊢ Itv (G) = Itv (G)$
7		eqid	$⊢ dist (G) = dist (G)$
8		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
9		eqid	$⊢ (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩)) = (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))$
10		eqid	$⊢ \leq_{𝒢}^{∠} (G) = \leq_{𝒢}^{∠} (G)$
11	1 2 6 7 3 8 9 4 10	angmgmval	$⊢ G \in 𝒢_{Tarski} \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} /_{𝑠} \underset{˙}{\sim}$
12	5 11	syl	$⊢ φ \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} /_{𝑠} \underset{˙}{\sim}$
13		ovex	$⊢ P^{(0 ..^3)} \in V$
14	2 13	rabex2	$⊢ A \in V$
15		1nn	$⊢ 1 \in ℕ$
16		basendx	$⊢ {Base}_{ndx} = 1$
17		1lt2	$⊢ 1 < 2$
18		2nn	$⊢ 2 \in ℕ$
19		plusgndx	$⊢ +_{ndx} = 2$
20		2lt10	$⊢ 2 < 10$
21		10nn	$⊢ 10 \in ℕ$
22		plendx	$⊢ \leq_{ndx} = 10$
23	15 16 17 18 19 20 21 22	strle3	$⊢ \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} Struct ⟨1, 10⟩$
24		baseid	$⊢ Base = Slot {Base}_{ndx}$
25		snsstp1	$⊢ \{⟨{Base}_{ndx}, A⟩\} \subseteq \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}$
26	23 24 25	strfv	$⊢ A \in V \to A = {Base}_{\{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}}$
27	14 26	mp1i	$⊢ φ \to A = {Base}_{\{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}}$
28	3	fvexi	$⊢ \underset{˙}{\sim} \in V$
29	28	a1i	$⊢ φ \to \underset{˙}{\sim} \in V$
30		tpex	$⊢ \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} \in V$
31	30	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, (e \in A, f \in A ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (G) e (2)), ⟨“ f (0) f (1) (ι z \in P \| (⟨“ f (2) f (1) z ”⟩ \underset{˙}{\sim} e \land f (1) dist (G) z = e (1) dist (G) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in P \| (⟨“ e (2) e (1) z ”⟩ \underset{˙}{\sim} f \land e (1) dist (G) z = f (1) dist (G) f (0) \land (e (1) {Line}_{𝒢} (G) e (2)) \cap (z Itv (G) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} \in V$
32	12 27 29 31	qusbas	$⊢ φ \to A / \underset{˙}{\sim} = {Base}_{J}$

Metamath Proof Explorer

Theorem angmgmbas

Proof