angmgmaddov1lem

	Ref	Expression
Hypotheses	angmgmadd.p	$⊢ P = {Base}_{G}$
	angmgmadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmgmadd.i	$⊢ I = Itv (G)$
	angmgmadd.d	$⊢ \underset{˙}{-} = dist (G)$
	angmgmadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmgmadd.l	$⊢ L = {Line}_{𝒢} (G)$
	angmgmadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmgmaddov.u	$⊢ φ \to U \in P$
	angmgmaddov.v	$⊢ φ \to V \in P$
	angmgmaddov.w	$⊢ φ \to W \in P$
	angmgmaddov.x	$⊢ φ \to X \in P$
	angmgmaddov.y	$⊢ φ \to Y \in P$
	angmgmaddov.z	$⊢ φ \to Z \in P$
	angmgmaddeu.1	$⊢ φ \to U \neq V$
	angmgmaddeu.2	$⊢ φ \to V \neq W$
	angmgmaddeu.3	$⊢ φ \to X \neq Y$
	angmgmaddeu.4	$⊢ φ \to Y \neq Z$
	angmgmaddov1lem.1	$⊢ φ \to \neg X \in (Y L Z)$
Assertion	angmgmaddov1lem	$⊢ φ \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		angmgmadd.p	$⊢ P = {Base}_{G}$
2		angmgmadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmgmadd.i	$⊢ I = Itv (G)$
4		angmgmadd.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmgmadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmgmadd.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmgmadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		angmgmaddov.u	$⊢ φ \to U \in P$
9		angmgmaddov.v	$⊢ φ \to V \in P$
10		angmgmaddov.w	$⊢ φ \to W \in P$
11		angmgmaddov.x	$⊢ φ \to X \in P$
12		angmgmaddov.y	$⊢ φ \to Y \in P$
13		angmgmaddov.z	$⊢ φ \to Z \in P$
14		angmgmaddeu.1	$⊢ φ \to U \neq V$
15		angmgmaddeu.2	$⊢ φ \to V \neq W$
16		angmgmaddeu.3	$⊢ φ \to X \neq Y$
17		angmgmaddeu.4	$⊢ φ \to Y \neq Z$
18		angmgmaddov1lem.1	$⊢ φ \to \neg X \in (Y L Z)$
19	7	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to G \in 𝒢_{Tarski}$
20	8	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to U \in P$
21	9	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to V \in P$
22	10	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to W \in P$
23	11	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to X \in P$
24	12	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to Y \in P$
25	13	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to Z \in P$
26	14	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to U \neq V$
27	15	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to V \neq W$
28	16	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to X \neq Y$
29	17	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to Y \neq Z$
30	18	adantr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to \neg X \in (Y L Z)$
31		simpr	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to U {hl}_{𝒢} (G) (V) W$
32	1 2 3 4 5 6 19 20 21 22 23 24 25 26 27 28 29 30 31	angmgmaddeu2	$⊢ (φ \land U {hl}_{𝒢} (G) (V) W) \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
33	32	adantlr	$⊢ ((φ \land U \in (V L W)) \land U {hl}_{𝒢} (G) (V) W) \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
34	7	adantr	$⊢ (φ \land V \in (W I U)) \to G \in 𝒢_{Tarski}$
35	8	adantr	$⊢ (φ \land V \in (W I U)) \to U \in P$
36	9	adantr	$⊢ (φ \land V \in (W I U)) \to V \in P$
37	10	adantr	$⊢ (φ \land V \in (W I U)) \to W \in P$
38	11	adantr	$⊢ (φ \land V \in (W I U)) \to X \in P$
39	12	adantr	$⊢ (φ \land V \in (W I U)) \to Y \in P$
40	13	adantr	$⊢ (φ \land V \in (W I U)) \to Z \in P$
41	14	adantr	$⊢ (φ \land V \in (W I U)) \to U \neq V$
42	15	adantr	$⊢ (φ \land V \in (W I U)) \to V \neq W$
43	16	adantr	$⊢ (φ \land V \in (W I U)) \to X \neq Y$
44	17	adantr	$⊢ (φ \land V \in (W I U)) \to Y \neq Z$
45	18	adantr	$⊢ (φ \land V \in (W I U)) \to \neg X \in (Y L Z)$
46		simpr	$⊢ (φ \land V \in (W I U)) \to V \in (W I U)$
47	1 4 3 34 37 36 35 46	tgbtwncom	$⊢ (φ \land V \in (W I U)) \to V \in (U I W)$
48	1 2 3 4 5 6 34 35 36 37 38 39 40 41 42 43 44 45 47	angmgmaddeu3	$⊢ (φ \land V \in (W I U)) \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
49	48	adantlr	$⊢ ((φ \land U \in (V L W)) \land V \in (W I U)) \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
50		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
51	10	adantr	$⊢ (φ \land U \in (V L W)) \to W \in P$
52	9	adantr	$⊢ (φ \land U \in (V L W)) \to V \in P$
53	8	adantr	$⊢ (φ \land U \in (V L W)) \to U \in P$
54	7	adantr	$⊢ (φ \land U \in (V L W)) \to G \in 𝒢_{Tarski}$
55	11	adantr	$⊢ (φ \land U \in (V L W)) \to X \in P$
56	15	necomd	$⊢ φ \to W \neq V$
57	56	adantr	$⊢ (φ \land U \in (V L W)) \to W \neq V$
58		simpr	$⊢ (φ \land U \in (V L W)) \to U \in (V L W)$
59	1 3 6 54 51 52 53 57 58	lncom	$⊢ (φ \land U \in (V L W)) \to U \in (W L V)$
60	1 3 50 51 52 53 54 55 6 59	lnhl	$⊢ (φ \land U \in (V L W)) \to (U {hl}_{𝒢} (G) (V) W \lor V \in (W I U))$
61	33 49 60	mpjaodan	$⊢ (φ \land U \in (V L W)) \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
62	7	adantr	$⊢ (φ \land \neg U \in (V L W)) \to G \in 𝒢_{Tarski}$
63	8	adantr	$⊢ (φ \land \neg U \in (V L W)) \to U \in P$
64	9	adantr	$⊢ (φ \land \neg U \in (V L W)) \to V \in P$
65	10	adantr	$⊢ (φ \land \neg U \in (V L W)) \to W \in P$
66	11	adantr	$⊢ (φ \land \neg U \in (V L W)) \to X \in P$
67	12	adantr	$⊢ (φ \land \neg U \in (V L W)) \to Y \in P$
68	13	adantr	$⊢ (φ \land \neg U \in (V L W)) \to Z \in P$
69	14	adantr	$⊢ (φ \land \neg U \in (V L W)) \to U \neq V$
70	15	adantr	$⊢ (φ \land \neg U \in (V L W)) \to V \neq W$
71	16	adantr	$⊢ (φ \land \neg U \in (V L W)) \to X \neq Y$
72	17	adantr	$⊢ (φ \land \neg U \in (V L W)) \to Y \neq Z$
73	18	adantr	$⊢ (φ \land \neg U \in (V L W)) \to \neg X \in (Y L Z)$
74		simpr	$⊢ (φ \land \neg U \in (V L W)) \to \neg U \in (V L W)$
75	1 2 3 4 5 6 62 63 64 65 66 67 68 69 70 71 72 73 74	angmgmaddeu1	$⊢ (φ \land \neg U \in (V L W)) \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
76	61 75	pm2.61dan	$⊢ φ \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$

Metamath Proof Explorer

Theorem angmgmaddov1lem

Proof