angmgmlem

	Ref	Expression
Hypotheses	angmgmval.p	$⊢ P = {Base}_{G}$
	angmgmval.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmgmval.i	$⊢ I = Itv (G)$
	angmgmval.d	$⊢ \underset{˙}{-} = dist (G)$
	angmgmval.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmgmval.l	$⊢ L = {Line}_{𝒢} (G)$
	angmgmval.o	$⊢ \underset{˙}{+} = (e \in A, f \in A ⟼ if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩))$
	angmgmval.j	No typesetting found for \|- J = ( AngMgm ` G ) with typecode \|-
	angmgmlem.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmgmlem.x	$⊢ φ \to X \in P$
	angmgmlem.y	$⊢ φ \to Y \in (P ∖ \{X\})$
Assertion	angmgmlem	$⊢ φ \to (J \in Mgm \land [⟨“ X Y X ”⟩] \underset{˙}{\sim} = 0_{J})$

Proof

Step	Hyp	Ref	Expression
1		angmgmval.p	$⊢ P = {Base}_{G}$
2		angmgmval.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmgmval.i	$⊢ I = Itv (G)$
4		angmgmval.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmgmval.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmgmval.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmgmval.o	$⊢ \underset{˙}{+} = (e \in A, f \in A ⟼ if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩))$
8		angmgmval.j	Could not format J = ( AngMgm ` G ) : No typesetting found for \|- J = ( AngMgm ` G ) with typecode \|-
9		angmgmlem.g	$⊢ φ \to G \in 𝒢_{Tarski}$
10		angmgmlem.x	$⊢ φ \to X \in P$
11		angmgmlem.y	$⊢ φ \to Y \in (P ∖ \{X\})$
12		eqid	$⊢ \leq_{𝒢}^{∠} (G) = \leq_{𝒢}^{∠} (G)$
13	1 2 3 4 5 6 7 8 12	angmgmval	$⊢ G \in 𝒢_{Tarski} \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} /_{𝑠} \underset{˙}{\sim}$
14	9 13	syl	$⊢ φ \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} /_{𝑠} \underset{˙}{\sim}$
15		ovex	$⊢ P^{(0 ..^3)} \in V$
16	2 15	rabex2	$⊢ A \in V$
17		1nn	$⊢ 1 \in ℕ$
18		basendx	$⊢ {Base}_{ndx} = 1$
19		1lt2	$⊢ 1 < 2$
20		2nn	$⊢ 2 \in ℕ$
21		plusgndx	$⊢ +_{ndx} = 2$
22		2lt10	$⊢ 2 < 10$
23		10nn	$⊢ 10 \in ℕ$
24		plendx	$⊢ \leq_{ndx} = 10$
25	17 18 19 20 21 22 23 24	strle3	$⊢ \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} Struct ⟨1, 10⟩$
26		baseid	$⊢ Base = Slot {Base}_{ndx}$
27		snsstp1	$⊢ \{⟨{Base}_{ndx}, A⟩\} \subseteq \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}$
28	25 26 27	strfv	$⊢ A \in V \to A = {Base}_{\{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}}$
29	16 28	mp1i	$⊢ φ \to A = {Base}_{\{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}}$
30	5	fvexi	$⊢ \underset{˙}{\sim} \in V$
31	30	a1i	$⊢ φ \to \underset{˙}{\sim} \in V$
32		tpex	$⊢ \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} \in V$
33	32	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} \in V$
34	1 2 5 9	cgrabasimass	$⊢ φ \to \underset{˙}{\sim} [A] \subseteq A$
35	14 29 31 33 34	qusin	$⊢ φ \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\} /_{𝑠} (\underset{˙}{\sim} \cap (A \times A))$
36	16 16	mpoex	$⊢ (e \in A, f \in A ⟼ if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩)) \in V$
37	7 36	eqeltri	$⊢ \underset{˙}{+} \in V$
38		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
39		snsstp2	$⊢ \{⟨+_{ndx}, \underset{˙}{+}⟩\} \subseteq \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}$
40	25 38 39	strfv	$⊢ \underset{˙}{+} \in V \to \underset{˙}{+} = +_{\{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}}$
41	37 40	ax-mp	$⊢ \underset{˙}{+} = +_{\{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (G)⟩\}}$
42	1 2 5 9	cgraer	$⊢ φ \to (\underset{˙}{\sim} \cap (A \times A)) Er A$
43	9	ad2antrr	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to G \in 𝒢_{Tarski}$
44		brinxp2	$⊢ a (\underset{˙}{\sim} \cap (A \times A)) p \leftrightarrow ((a \in A \land p \in A) \land a \underset{˙}{\sim} p)$
45	44	biimpi	$⊢ a (\underset{˙}{\sim} \cap (A \times A)) p \to ((a \in A \land p \in A) \land a \underset{˙}{\sim} p)$
46	45	ad2antlr	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to ((a \in A \land p \in A) \land a \underset{˙}{\sim} p)$
47	46	simplld	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to a \in A$
48		brinxp2	$⊢ b (\underset{˙}{\sim} \cap (A \times A)) q \leftrightarrow ((b \in A \land q \in A) \land b \underset{˙}{\sim} q)$
49	48	bilani	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to ((b \in A \land q \in A) \land b \underset{˙}{\sim} q)$
50	49	simplld	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to b \in A$
51	1 2 3 4 5 6 43 7 47 50	angmgmaddcl	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to a \underset{˙}{+} b \in A$
52	46	simplrd	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to p \in A$
53	49	simplrd	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to q \in A$
54	1 2 3 4 5 6 43 7 52 53	angmgmaddcl	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to p \underset{˙}{+} q \in A$
55	46	simprd	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to a \underset{˙}{\sim} p$
56	49	simprd	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to b \underset{˙}{\sim} q$
57	1 2 3 4 5 6 43 7 52 53 47 50 55 56	angmgmaddcpbl	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q)$
58		brinxp2	$⊢ (a \underset{˙}{+} b) (\underset{˙}{\sim} \cap (A \times A)) (p \underset{˙}{+} q) \leftrightarrow ((a \underset{˙}{+} b \in A \land p \underset{˙}{+} q \in A) \land (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
59	51 54 57 58	syl21anbrc	$⊢ ((φ \land a (\underset{˙}{\sim} \cap (A \times A)) p) \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to (a \underset{˙}{+} b) (\underset{˙}{\sim} \cap (A \times A)) (p \underset{˙}{+} q)$
60	59	expl	$⊢ φ \to ((a (\underset{˙}{\sim} \cap (A \times A)) p \land b (\underset{˙}{\sim} \cap (A \times A)) q) \to (a \underset{˙}{+} b) (\underset{˙}{\sim} \cap (A \times A)) (p \underset{˙}{+} q))$
61	9	3ad2ant1	$⊢ (φ \land i \in A \land j \in A) \to G \in 𝒢_{Tarski}$
62		simp2	$⊢ (φ \land i \in A \land j \in A) \to i \in A$
63		simp3	$⊢ (φ \land i \in A \land j \in A) \to j \in A$
64	1 2 3 4 5 6 61 7 62 63	angmgmaddcl	$⊢ (φ \land i \in A \land j \in A) \to i \underset{˙}{+} j \in A$
65	1	fvexi	$⊢ P \in V$
66	65	a1i	$⊢ φ \to P \in V$
67	11	eldifad	$⊢ φ \to Y \in P$
68	11	eldifsnbd	$⊢ φ \to Y \neq X$
69	68	necomd	$⊢ φ \to X \neq Y$
70	2 66 10 67 10 69 68	elcgrabasrd	$⊢ φ \to ⟨“ X Y X ”⟩ \in A$
71	9	adantr	$⊢ (φ \land i \in A) \to G \in 𝒢_{Tarski}$
72	70	adantr	$⊢ (φ \land i \in A) \to ⟨“ X Y X ”⟩ \in A$
73		simpr	$⊢ (φ \land i \in A) \to i \in A$
74	1 2 3 4 5 6 71 7 72 73	angmgmaddcl	$⊢ (φ \land i \in A) \to ⟨“ X Y X ”⟩ \underset{˙}{+} i \in A$
75	10	adantr	$⊢ (φ \land i \in A) \to X \in P$
76	11	adantr	$⊢ (φ \land i \in A) \to Y \in (P ∖ \{X\})$
77	1 2 3 4 5 6 71 7 75 76 73	angmgmaddlid	$⊢ (φ \land i \in A) \to (⟨“ X Y X ”⟩ \underset{˙}{+} i) \underset{˙}{\sim} i$
78		brinxp2	$⊢ (⟨“ X Y X ”⟩ \underset{˙}{+} i) (\underset{˙}{\sim} \cap (A \times A)) i \leftrightarrow ((⟨“ X Y X ”⟩ \underset{˙}{+} i \in A \land i \in A) \land (⟨“ X Y X ”⟩ \underset{˙}{+} i) \underset{˙}{\sim} i)$
79	74 73 77 78	syl21anbrc	$⊢ (φ \land i \in A) \to (⟨“ X Y X ”⟩ \underset{˙}{+} i) (\underset{˙}{\sim} \cap (A \times A)) i$
80	1 2 3 4 5 6 71 7 73 72	angmgmaddcl	$⊢ (φ \land i \in A) \to i \underset{˙}{+} ⟨“ X Y X ”⟩ \in A$
81	1 2 3 4 5 6 71 7 75 76 73	angmgmaddrid	$⊢ (φ \land i \in A) \to (i \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} i$
82		brinxp2	$⊢ (i \underset{˙}{+} ⟨“ X Y X ”⟩) (\underset{˙}{\sim} \cap (A \times A)) i \leftrightarrow ((i \underset{˙}{+} ⟨“ X Y X ”⟩ \in A \land i \in A) \land (i \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} i)$
83	80 73 81 82	syl21anbrc	$⊢ (φ \land i \in A) \to (i \underset{˙}{+} ⟨“ X Y X ”⟩) (\underset{˙}{\sim} \cap (A \times A)) i$
84	35 29 41 42 33 60 64 70 79 83	qusmgm	$⊢ φ \to (J \in Mgm \land [⟨“ X Y X ”⟩] (\underset{˙}{\sim} \cap (A \times A)) = 0_{J})$
85		ecinxp	$⊢ (\underset{˙}{\sim} [A] \subseteq A \land ⟨“ X Y X ”⟩ \in A) \to [⟨“ X Y X ”⟩] \underset{˙}{\sim} = [⟨“ X Y X ”⟩] (\underset{˙}{\sim} \cap (A \times A))$
86	34 70 85	syl2anc	$⊢ φ \to [⟨“ X Y X ”⟩] \underset{˙}{\sim} = [⟨“ X Y X ”⟩] (\underset{˙}{\sim} \cap (A \times A))$
87	86	eqeq1d	$⊢ φ \to ([⟨“ X Y X ”⟩] \underset{˙}{\sim} = 0_{J} \leftrightarrow [⟨“ X Y X ”⟩] (\underset{˙}{\sim} \cap (A \times A)) = 0_{J})$
88	87	anbi2d	$⊢ φ \to ((J \in Mgm \land [⟨“ X Y X ”⟩] \underset{˙}{\sim} = 0_{J}) \leftrightarrow (J \in Mgm \land [⟨“ X Y X ”⟩] (\underset{˙}{\sim} \cap (A \times A)) = 0_{J}))$
89	84 88	mpbird	$⊢ φ \to (J \in Mgm \land [⟨“ X Y X ”⟩] \underset{˙}{\sim} = 0_{J})$

Metamath Proof Explorer

Theorem angmgmlem

Proof