angmndaddov1

Description: Value of the addition operation in the angle addition monoid, in case the first angle is neither zero nor flat. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	angmndadd.p	$⊢ P = {Base}_{G}$
	angmndadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmndadd.i	$⊢ I = Itv (G)$
	angmndadd.d	$⊢ \underset{˙}{-} = dist (G)$
	angmndadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmndadd.l	$⊢ L = {Line}_{𝒢} (G)$
	angmndadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmndaddov.u	$⊢ φ \to U \in P$
	angmndaddov.v	$⊢ φ \to V \in P$
	angmndaddov.w	$⊢ φ \to W \in P$
	angmndaddov.x	$⊢ φ \to X \in P$
	angmndaddov.y	$⊢ φ \to Y \in P$
	angmndaddov.z	$⊢ φ \to Z \in P$
	angmndaddeu.1	$⊢ φ \to U \neq V$
	angmndaddeu.2	$⊢ φ \to V \neq W$
	angmndaddeu.3	$⊢ φ \to X \neq Y$
	angmndaddeu.4	$⊢ φ \to Y \neq Z$
	angmndaddov.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)) ”⟩))$
	angmndaddov1.x	$⊢ φ \to \neg X \in (Y L Z)$
	angmndaddov1.s	$⊢ φ \to S \in P$
	angmndaddov1.1	$⊢ φ \to ⟨“ Z Y S ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
	angmndaddov1.2	$⊢ φ \to Y \underset{˙}{-} S = V \underset{˙}{-} U$
	angmndaddov1.3	$⊢ φ \to (Y L Z) \cap (S I X) \neq \emptyset$
Assertion	angmndaddov1	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{+} ⟨“ U V W ”⟩ = ⟨“ X Y S ”⟩$

Proof

Step	Hyp	Ref	Expression
1		angmndadd.p	$⊢ P = {Base}_{G}$
2		angmndadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmndadd.i	$⊢ I = Itv (G)$
4		angmndadd.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmndadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmndadd.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmndadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		angmndaddov.u	$⊢ φ \to U \in P$
9		angmndaddov.v	$⊢ φ \to V \in P$
10		angmndaddov.w	$⊢ φ \to W \in P$
11		angmndaddov.x	$⊢ φ \to X \in P$
12		angmndaddov.y	$⊢ φ \to Y \in P$
13		angmndaddov.z	$⊢ φ \to Z \in P$
14		angmndaddeu.1	$⊢ φ \to U \neq V$
15		angmndaddeu.2	$⊢ φ \to V \neq W$
16		angmndaddeu.3	$⊢ φ \to X \neq Y$
17		angmndaddeu.4	$⊢ φ \to Y \neq Z$
18		angmndaddov.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)) ”⟩))$
19		angmndaddov1.x	$⊢ φ \to \neg X \in (Y L Z)$
20		angmndaddov1.s	$⊢ φ \to S \in P$
21		angmndaddov1.1	$⊢ φ \to ⟨“ Z Y S ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
22		angmndaddov1.2	$⊢ φ \to Y \underset{˙}{-} S = V \underset{˙}{-} U$
23		angmndaddov1.3	$⊢ φ \to (Y L Z) \cap (S I X) \neq \emptyset$
24	18	a1i	$⊢ φ \to \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)) ”⟩))$
25		simplr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e = ⟨“ X Y Z ”⟩$
26	25	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (0) = ⟨“ X Y Z ”⟩ (0)$
27		s3fv0	$⊢ X \in P \to ⟨“ X Y Z ”⟩ (0) = X$
28	11 27	syl	$⊢ φ \to ⟨“ X Y Z ”⟩ (0) = X$
29	28	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ X Y Z ”⟩ (0) = X$
30	26 29	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (0) = X$
31	19	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \neg X \in (Y L Z)$
32	25	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) = ⟨“ X Y Z ”⟩ (1)$
33		s3fv1	$⊢ Y \in P \to ⟨“ X Y Z ”⟩ (1) = Y$
34	12 33	syl	$⊢ φ \to ⟨“ X Y Z ”⟩ (1) = Y$
35	34	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ X Y Z ”⟩ (1) = Y$
36	32 35	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) = Y$
37	25	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (2) = ⟨“ X Y Z ”⟩ (2)$
38		s3fv2	$⊢ Z \in P \to ⟨“ X Y Z ”⟩ (2) = Z$
39	13 38	syl	$⊢ φ \to ⟨“ X Y Z ”⟩ (2) = Z$
40	39	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ X Y Z ”⟩ (2) = Z$
41	37 40	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (2) = Z$
42	36 41	oveq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) L e (2) = Y L Z$
43	31 42	neleqtrrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \neg X \in (e (1) L e (2))$
44	30 43	eqneltrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \neg e (0) \in (e (1) L e (2))$
45	44	iffalsed	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to 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)) ”⟩) = ⟨“ 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)) ”⟩$
46	20	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to S \in P$
47	7	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to G \in 𝒢_{Tarski}$
48	8	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to U \in P$
49	9	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to V \in P$
50	10	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to W \in P$
51	11	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to X \in P$
52	12	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Y \in P$
53	36 52	eqeltrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) \in P$
54	13	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Z \in P$
55	41 54	eqeltrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (2) \in P$
56	14	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to U \neq V$
57	15	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to V \neq W$
58	16	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to X \neq Y$
59	58 36	neeqtrrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to X \neq e (1)$
60	17	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Y \neq Z$
61	36 60	eqnetrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) \neq Z$
62	61 41	neeqtrrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) \neq e (2)$
63	1 2 3 4 5 6 47 48 49 50 51 53 55 56 57 59 62 43	angmndaddov1lem	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \exists! s \in P (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land e (1) \underset{˙}{-} s = V \underset{˙}{-} U \land (e (1) L e (2)) \cap (s I X) \neq \emptyset)$
64		simpr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f = ⟨“ U V W ”⟩$
65	64	breq2d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \leftrightarrow ⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩)$
66	64	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) = ⟨“ U V W ”⟩ (1)$
67		s3fv1	$⊢ V \in P \to ⟨“ U V W ”⟩ (1) = V$
68	9 67	syl	$⊢ φ \to ⟨“ U V W ”⟩ (1) = V$
69	68	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ U V W ”⟩ (1) = V$
70	66 69	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) = V$
71	64	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (0) = ⟨“ U V W ”⟩ (0)$
72		s3fv0	$⊢ U \in P \to ⟨“ U V W ”⟩ (0) = U$
73	8 72	syl	$⊢ φ \to ⟨“ U V W ”⟩ (0) = U$
74	73	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ U V W ”⟩ (0) = U$
75	71 74	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (0) = U$
76	70 75	oveq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) \underset{˙}{-} f (0) = V \underset{˙}{-} U$
77	76	eqeq2d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \leftrightarrow e (1) \underset{˙}{-} s = V \underset{˙}{-} U)$
78	30	oveq2d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to s I e (0) = s I X$
79	78	ineq2d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (e (1) L e (2)) \cap (s I e (0)) = (e (1) L e (2)) \cap (s I X)$
80	79	neeq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ((e (1) L e (2)) \cap (s I e (0)) \neq \emptyset \leftrightarrow (e (1) L e (2)) \cap (s I X) \neq \emptyset)$
81	65 77 80	3anbi123d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ((⟨“ 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) \leftrightarrow (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land e (1) \underset{˙}{-} s = V \underset{˙}{-} U \land (e (1) L e (2)) \cap (s I X) \neq \emptyset))$
82	81	reubidv	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (\exists! 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) \leftrightarrow \exists! s \in P (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land e (1) \underset{˙}{-} s = V \underset{˙}{-} U \land (e (1) L e (2)) \cap (s I X) \neq \emptyset))$
83	63 82	mpbird	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \exists! 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)$
84	21	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ Z Y S ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
85		eqidd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to S = S$
86	41 36 85	s3eqd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ e (2) e (1) S ”⟩ = ⟨“ Z Y S ”⟩$
87	84 86 64	3brtr4d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ e (2) e (1) S ”⟩ \underset{˙}{\sim} f$
88	22	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Y \underset{˙}{-} S = V \underset{˙}{-} U$
89	36	oveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) \underset{˙}{-} S = Y \underset{˙}{-} S$
90	88 89 76	3eqtr4d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) \underset{˙}{-} S = f (1) \underset{˙}{-} f (0)$
91	30	oveq2d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to S I e (0) = S I X$
92	42 91	ineq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (e (1) L e (2)) \cap (S I e (0)) = (Y L Z) \cap (S I X)$
93	23	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (Y L Z) \cap (S I X) \neq \emptyset$
94	92 93	eqnetrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (e (1) L e (2)) \cap (S I e (0)) \neq \emptyset$
95		eqidd	$⊢ s = S \to e (2) = e (2)$
96		eqidd	$⊢ s = S \to e (1) = e (1)$
97		id	$⊢ s = S \to s = S$
98	95 96 97	s3eqd	$⊢ s = S \to ⟨“ e (2) e (1) s ”⟩ = ⟨“ e (2) e (1) S ”⟩$
99	98	breq1d	$⊢ s = S \to (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \leftrightarrow ⟨“ e (2) e (1) S ”⟩ \underset{˙}{\sim} f)$
100		oveq2	$⊢ s = S \to e (1) \underset{˙}{-} s = e (1) \underset{˙}{-} S$
101	100	eqeq1d	$⊢ s = S \to (e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \leftrightarrow e (1) \underset{˙}{-} S = f (1) \underset{˙}{-} f (0))$
102		oveq1	$⊢ s = S \to s I e (0) = S I e (0)$
103	102	ineq2d	$⊢ s = S \to (e (1) L e (2)) \cap (s I e (0)) = (e (1) L e (2)) \cap (S I e (0))$
104	103	neeq1d	$⊢ s = S \to ((e (1) L e (2)) \cap (s I e (0)) \neq \emptyset \leftrightarrow (e (1) L e (2)) \cap (S I e (0)) \neq \emptyset)$
105	99 101 104	3anbi123d	$⊢ s = S \to ((⟨“ 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) \leftrightarrow (⟨“ 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))$
106	105	riota2	$⊢ (S \in P \land \exists! 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)) \to ((⟨“ 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) \leftrightarrow (ι 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)) = S)$
107	106	biimpa	$⊢ ((S \in P \land \exists! 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)) \land (⟨“ 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)) \to (ι 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)) = S$
108	46 83 87 90 94 107	syl23anc	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (ι 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)) = S$
109	30 36 108	s3eqd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ 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)) ”⟩ = ⟨“ X Y S ”⟩$
110	45 109	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to 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)) ”⟩) = ⟨“ X Y S ”⟩$
111	110	anasss	$⊢ (φ \land (e = ⟨“ X Y Z ”⟩ \land f = ⟨“ U V W ”⟩)) \to 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)) ”⟩) = ⟨“ X Y S ”⟩$
112	1	fvexi	$⊢ P \in V$
113	112	a1i	$⊢ φ \to P \in V$
114	2 113 11 12 13 16 17	elcgrabasrd	$⊢ φ \to ⟨“ X Y Z ”⟩ \in A$
115	2 113 8 9 10 14 15	elcgrabasrd	$⊢ φ \to ⟨“ U V W ”⟩ \in A$
116	22	eqcomd	$⊢ φ \to V \underset{˙}{-} U = Y \underset{˙}{-} S$
117	14	necomd	$⊢ φ \to V \neq U$
118	1 4 3 7 9 8 12 20 116 117	tgcgrneq	$⊢ φ \to Y \neq S$
119	2 113 11 12 20 16 118	elcgrabasrd	$⊢ φ \to ⟨“ X Y S ”⟩ \in A$
120	24 111 114 115 119	ovmpod	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{+} ⟨“ U V W ”⟩ = ⟨“ X Y S ”⟩$

Metamath Proof Explorer

Theorem angmndaddov1

Proof