angmgmaddov2

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

	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$
	angmgmaddov.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)) ”⟩))$
	angmgmaddov2.x	$⊢ φ \to X \in (Y L Z)$
	angmgmaddov2.s	$⊢ φ \to S \in P$
	angmgmaddov2.1	$⊢ φ \to ⟨“ W V S ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
	angmgmaddov2.2	$⊢ φ \to V \underset{˙}{-} S = Y \underset{˙}{-} X$
Assertion	angmgmaddov2	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{+} ⟨“ U V W ”⟩ = ⟨“ U V S ”⟩$

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		angmgmaddov.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		angmgmaddov2.x	$⊢ φ \to X \in (Y L Z)$
20		angmgmaddov2.s	$⊢ φ \to S \in P$
21		angmgmaddov2.1	$⊢ φ \to ⟨“ W V S ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
22		angmgmaddov2.2	$⊢ φ \to V \underset{˙}{-} S = Y \underset{˙}{-} X$
23	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)) ”⟩))$
24	19	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to X \in (Y L Z)$
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	25	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) = ⟨“ X Y Z ”⟩ (1)$
32		s3fv1	$⊢ Y \in P \to ⟨“ X Y Z ”⟩ (1) = Y$
33	12 32	syl	$⊢ φ \to ⟨“ X Y Z ”⟩ (1) = Y$
34	33	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ X Y Z ”⟩ (1) = Y$
35	31 34	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) = Y$
36	25	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (2) = ⟨“ X Y Z ”⟩ (2)$
37		s3fv2	$⊢ Z \in P \to ⟨“ X Y Z ”⟩ (2) = Z$
38	13 37	syl	$⊢ φ \to ⟨“ X Y Z ”⟩ (2) = Z$
39	38	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ X Y Z ”⟩ (2) = Z$
40	36 39	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (2) = Z$
41	35 40	oveq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) L e (2) = Y L Z$
42	24 30 41	3eltr4d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (0) \in (e (1) L e (2))$
43	42	iftrued	$⊢ ((φ \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)) ”⟩) = ⟨“ 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))) ”⟩$
44		simpr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f = ⟨“ U V W ”⟩$
45	44	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (0) = ⟨“ U V W ”⟩ (0)$
46		s3fv0	$⊢ U \in P \to ⟨“ U V W ”⟩ (0) = U$
47	8 46	syl	$⊢ φ \to ⟨“ U V W ”⟩ (0) = U$
48	47	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ U V W ”⟩ (0) = U$
49	45 48	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (0) = U$
50	44	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) = ⟨“ U V W ”⟩ (1)$
51		s3fv1	$⊢ V \in P \to ⟨“ U V W ”⟩ (1) = V$
52	9 51	syl	$⊢ φ \to ⟨“ U V W ”⟩ (1) = V$
53	52	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ U V W ”⟩ (1) = V$
54	50 53	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) = V$
55	20	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to S \in P$
56	7	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to G \in 𝒢_{Tarski}$
57	10	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to W \in P$
58	9	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to V \in P$
59	11	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to X \in P$
60	12	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Y \in P$
61	13	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Z \in P$
62	15	necomd	$⊢ φ \to W \neq V$
63	62	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to W \neq V$
64	15	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to V \neq W$
65	16	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to X \neq Y$
66	17	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to Y \neq Z$
67	1 2 3 4 5 6 56 57 58 57 59 60 61 63 64 65 66 24	angmgmaddov2lem	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
68	44	fveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (2) = ⟨“ U V W ”⟩ (2)$
69		s3fv2	$⊢ W \in P \to ⟨“ U V W ”⟩ (2) = W$
70	10 69	syl	$⊢ φ \to ⟨“ U V W ”⟩ (2) = W$
71	70	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ U V W ”⟩ (2) = W$
72	68 71	eqtrd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (2) = W$
73		eqidd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to s = s$
74	72 54 73	s3eqd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ f (2) f (1) s ”⟩ = ⟨“ W V s ”⟩$
75	74 25	breq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \leftrightarrow ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩)$
76	54	oveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) \underset{˙}{-} s = V \underset{˙}{-} s$
77	35 30	oveq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to e (1) \underset{˙}{-} e (0) = Y \underset{˙}{-} X$
78	76 77	eqeq12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0) \leftrightarrow V \underset{˙}{-} s = Y \underset{˙}{-} X)$
79	75 78	anbi12d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ((⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0)) \leftrightarrow (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X))$
80	79	bicomd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ((⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \leftrightarrow (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0)))$
81	80	reubidv	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (\exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \leftrightarrow \exists! s \in P (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0)))$
82	67 81	mpbid	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to \exists! s \in P (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))$
83	21	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ W V S ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
84		eqidd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to S = S$
85	72 54 84	s3eqd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ f (2) f (1) S ”⟩ = ⟨“ W V S ”⟩$
86	83 85 25	3brtr4d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ f (2) f (1) S ”⟩ \underset{˙}{\sim} e$
87	22	ad2antrr	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to V \underset{˙}{-} S = Y \underset{˙}{-} X$
88	54	oveq1d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) \underset{˙}{-} S = V \underset{˙}{-} S$
89	87 88 77	3eqtr4d	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to f (1) \underset{˙}{-} S = e (1) \underset{˙}{-} e (0)$
90		eqidd	$⊢ s = S \to f (2) = f (2)$
91		eqidd	$⊢ s = S \to f (1) = f (1)$
92		id	$⊢ s = S \to s = S$
93	90 91 92	s3eqd	$⊢ s = S \to ⟨“ f (2) f (1) s ”⟩ = ⟨“ f (2) f (1) S ”⟩$
94	93	breq1d	$⊢ s = S \to (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \leftrightarrow ⟨“ f (2) f (1) S ”⟩ \underset{˙}{\sim} e)$
95		oveq2	$⊢ s = S \to f (1) \underset{˙}{-} s = f (1) \underset{˙}{-} S$
96	95	eqeq1d	$⊢ s = S \to (f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0) \leftrightarrow f (1) \underset{˙}{-} S = e (1) \underset{˙}{-} e (0))$
97	94 96	anbi12d	$⊢ s = S \to ((⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0)) \leftrightarrow (⟨“ f (2) f (1) S ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} S = e (1) \underset{˙}{-} e (0)))$
98	97	riota2	$⊢ (S \in P \land \exists! s \in P (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) \to ((⟨“ f (2) f (1) S ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} S = e (1) \underset{˙}{-} e (0)) \leftrightarrow (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) = S)$
99	98	biimpa	$⊢ ((S \in P \land \exists! s \in P (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) \land (⟨“ f (2) f (1) S ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} S = e (1) \underset{˙}{-} e (0))) \to (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) = S$
100	55 82 86 89 99	syl22anc	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) = S$
101	49 54 100	s3eqd	$⊢ ((φ \land e = ⟨“ X Y Z ”⟩) \land f = ⟨“ U V W ”⟩) \to ⟨“ 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))) ”⟩ = ⟨“ U V S ”⟩$
102	43 101	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)) ”⟩) = ⟨“ U V S ”⟩$
103	102	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)) ”⟩) = ⟨“ U V S ”⟩$
104	1	fvexi	$⊢ P \in V$
105	104	a1i	$⊢ φ \to P \in V$
106	2 105 11 12 13 16 17	elcgrabasrd	$⊢ φ \to ⟨“ X Y Z ”⟩ \in A$
107	2 105 8 9 10 14 15	elcgrabasrd	$⊢ φ \to ⟨“ U V W ”⟩ \in A$
108	22	eqcomd	$⊢ φ \to Y \underset{˙}{-} X = V \underset{˙}{-} S$
109	16	necomd	$⊢ φ \to Y \neq X$
110	1 4 3 7 12 11 9 20 108 109	tgcgrneq	$⊢ φ \to V \neq S$
111	2 105 8 9 20 14 110	elcgrabasrd	$⊢ φ \to ⟨“ U V S ”⟩ \in A$
112	23 103 106 107 111	ovmpod	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{+} ⟨“ U V W ”⟩ = ⟨“ U V S ”⟩$

Metamath Proof Explorer

Theorem angmgmaddov2

Proof