cyc3co2

Description: Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023)

	Ref	Expression
Hypotheses	cycpm3.c	$⊢ C = toCyc (D)$
	cycpm3.s	$⊢ S = SymGrp (D)$
	cycpm3.d	$⊢ φ \to D \in V$
	cycpm3.i	$⊢ φ \to I \in D$
	cycpm3.j	$⊢ φ \to J \in D$
	cycpm3.k	$⊢ φ \to K \in D$
	cycpm3.1	$⊢ φ \to I \neq J$
	cycpm3.2	$⊢ φ \to J \neq K$
	cycpm3.3	$⊢ φ \to K \neq I$
	cyc3co2.t	$⊢ \underset{˙}{\cdot} = +_{S}$
Assertion	cyc3co2	$⊢ φ \to C (⟨“ I J K ”⟩) = C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		cycpm3.c	$⊢ C = toCyc (D)$
2		cycpm3.s	$⊢ S = SymGrp (D)$
3		cycpm3.d	$⊢ φ \to D \in V$
4		cycpm3.i	$⊢ φ \to I \in D$
5		cycpm3.j	$⊢ φ \to J \in D$
6		cycpm3.k	$⊢ φ \to K \in D$
7		cycpm3.1	$⊢ φ \to I \neq J$
8		cycpm3.2	$⊢ φ \to J \neq K$
9		cycpm3.3	$⊢ φ \to K \neq I$
10		cyc3co2.t	$⊢ \underset{˙}{\cdot} = +_{S}$
11	1 2 3 4 5 6 7 8 9	cycpm3cl	$⊢ φ \to C (⟨“ I J K ”⟩) \in {Base}_{S}$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13	2 12	symgbasf	$⊢ C (⟨“ I J K ”⟩) \in {Base}_{S} \to C (⟨“ I J K ”⟩) : D ⟶ D$
14	11 13	syl	$⊢ φ \to C (⟨“ I J K ”⟩) : D ⟶ D$
15	14	ffnd	$⊢ φ \to C (⟨“ I J K ”⟩) Fn D$
16	2	symggrp	$⊢ D \in V \to S \in Grp$
17	3 16	syl	$⊢ φ \to S \in Grp$
18	9	necomd	$⊢ φ \to I \neq K$
19	1 3 4 6 18 2	cycpm2cl	$⊢ φ \to C (⟨“ I K ”⟩) \in {Base}_{S}$
20	1 3 4 5 7 2	cycpm2cl	$⊢ φ \to C (⟨“ I J ”⟩) \in {Base}_{S}$
21	12 10	grpcl	$⊢ (S \in Grp \land C (⟨“ I K ”⟩) \in {Base}_{S} \land C (⟨“ I J ”⟩) \in {Base}_{S}) \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) \in {Base}_{S}$
22	17 19 20 21	syl3anc	$⊢ φ \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) \in {Base}_{S}$
23	2 12	symgbasf	$⊢ C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) \in {Base}_{S} \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) : D ⟶ D$
24	22 23	syl	$⊢ φ \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) : D ⟶ D$
25	24	ffnd	$⊢ φ \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) Fn D$
26	1 2 3 4 5 6 7 8 9	cyc3fv1	$⊢ φ \to C (⟨“ I J K ”⟩) (I) = J$
27	26	adantr	$⊢ (φ \land x = I) \to C (⟨“ I J K ”⟩) (I) = J$
28		simpr	$⊢ (φ \land x = I) \to x = I$
29	28	fveq2d	$⊢ (φ \land x = I) \to C (⟨“ I J K ”⟩) (x) = C (⟨“ I J K ”⟩) (I)$
30	2 12 10	symgov	$⊢ (C (⟨“ I K ”⟩) \in {Base}_{S} \land C (⟨“ I J ”⟩) \in {Base}_{S}) \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) = C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)$
31	19 20 30	syl2anc	$⊢ φ \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) = C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)$
32	31	adantr	$⊢ (φ \land x = I) \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) = C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)$
33	32	fveq1d	$⊢ (φ \land x = I) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x)$
34	2 12	symgbasf	$⊢ C (⟨“ I J ”⟩) \in {Base}_{S} \to C (⟨“ I J ”⟩) : D ⟶ D$
35	20 34	syl	$⊢ φ \to C (⟨“ I J ”⟩) : D ⟶ D$
36	35	ffund	$⊢ φ \to Fun C (⟨“ I J ”⟩)$
37	4	adantr	$⊢ (φ \land x = I) \to I \in D$
38	34	fdmd	$⊢ C (⟨“ I J ”⟩) \in {Base}_{S} \to dom C (⟨“ I J ”⟩) = D$
39	20 38	syl	$⊢ φ \to dom C (⟨“ I J ”⟩) = D$
40	39	adantr	$⊢ (φ \land x = I) \to dom C (⟨“ I J ”⟩) = D$
41	37 28 40	3eltr4d	$⊢ (φ \land x = I) \to x \in dom C (⟨“ I J ”⟩)$
42		fvco	$⊢ (Fun C (⟨“ I J ”⟩) \land x \in dom C (⟨“ I J ”⟩)) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x))$
43	36 41 42	syl2an2r	$⊢ (φ \land x = I) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x))$
44	28	fveq2d	$⊢ (φ \land x = I) \to C (⟨“ I J ”⟩) (x) = C (⟨“ I J ”⟩) (I)$
45	1 3 4 5 7 2	cyc2fv1	$⊢ φ \to C (⟨“ I J ”⟩) (I) = J$
46	45	adantr	$⊢ (φ \land x = I) \to C (⟨“ I J ”⟩) (I) = J$
47	44 46	eqtrd	$⊢ (φ \land x = I) \to C (⟨“ I J ”⟩) (x) = J$
48	47	fveq2d	$⊢ (φ \land x = I) \to C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x)) = C (⟨“ I K ”⟩) (J)$
49	8	necomd	$⊢ φ \to K \neq J$
50	7	necomd	$⊢ φ \to J \neq I$
51	1 2 3 4 6 5 18 49 50	cyc2fvx	$⊢ φ \to C (⟨“ I K ”⟩) (J) = J$
52	51	adantr	$⊢ (φ \land x = I) \to C (⟨“ I K ”⟩) (J) = J$
53	43 48 52	3eqtrd	$⊢ (φ \land x = I) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = J$
54	33 53	eqtrd	$⊢ (φ \land x = I) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = J$
55	27 29 54	3eqtr4d	$⊢ (φ \land x = I) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
56	55	adantlr	$⊢ ((φ \land x \in \{I, J, K\}) \land x = I) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
57	1 2 3 4 5 6 7 8 9	cyc3fv2	$⊢ φ \to C (⟨“ I J K ”⟩) (J) = K$
58	57	adantr	$⊢ (φ \land x = J) \to C (⟨“ I J K ”⟩) (J) = K$
59		simpr	$⊢ (φ \land x = J) \to x = J$
60	59	fveq2d	$⊢ (φ \land x = J) \to C (⟨“ I J K ”⟩) (x) = C (⟨“ I J K ”⟩) (J)$
61	31	adantr	$⊢ (φ \land x = J) \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) = C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)$
62	61	fveq1d	$⊢ (φ \land x = J) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x)$
63	5	adantr	$⊢ (φ \land x = J) \to J \in D$
64	39	adantr	$⊢ (φ \land x = J) \to dom C (⟨“ I J ”⟩) = D$
65	63 59 64	3eltr4d	$⊢ (φ \land x = J) \to x \in dom C (⟨“ I J ”⟩)$
66	36 65 42	syl2an2r	$⊢ (φ \land x = J) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x))$
67	59	fveq2d	$⊢ (φ \land x = J) \to C (⟨“ I J ”⟩) (x) = C (⟨“ I J ”⟩) (J)$
68	1 3 4 5 7 2	cyc2fv2	$⊢ φ \to C (⟨“ I J ”⟩) (J) = I$
69	68	adantr	$⊢ (φ \land x = J) \to C (⟨“ I J ”⟩) (J) = I$
70	67 69	eqtrd	$⊢ (φ \land x = J) \to C (⟨“ I J ”⟩) (x) = I$
71	70	fveq2d	$⊢ (φ \land x = J) \to C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x)) = C (⟨“ I K ”⟩) (I)$
72	1 3 4 6 18 2	cyc2fv1	$⊢ φ \to C (⟨“ I K ”⟩) (I) = K$
73	72	adantr	$⊢ (φ \land x = J) \to C (⟨“ I K ”⟩) (I) = K$
74	66 71 73	3eqtrd	$⊢ (φ \land x = J) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = K$
75	62 74	eqtrd	$⊢ (φ \land x = J) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = K$
76	58 60 75	3eqtr4d	$⊢ (φ \land x = J) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
77	76	adantlr	$⊢ ((φ \land x \in \{I, J, K\}) \land x = J) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
78	1 2 3 4 5 6 7 8 9	cyc3fv3	$⊢ φ \to C (⟨“ I J K ”⟩) (K) = I$
79	78	adantr	$⊢ (φ \land x = K) \to C (⟨“ I J K ”⟩) (K) = I$
80		simpr	$⊢ (φ \land x = K) \to x = K$
81	80	fveq2d	$⊢ (φ \land x = K) \to C (⟨“ I J K ”⟩) (x) = C (⟨“ I J K ”⟩) (K)$
82	31	adantr	$⊢ (φ \land x = K) \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) = C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)$
83	82	fveq1d	$⊢ (φ \land x = K) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x)$
84	6	adantr	$⊢ (φ \land x = K) \to K \in D$
85	39	adantr	$⊢ (φ \land x = K) \to dom C (⟨“ I J ”⟩) = D$
86	84 80 85	3eltr4d	$⊢ (φ \land x = K) \to x \in dom C (⟨“ I J ”⟩)$
87	36 86 42	syl2an2r	$⊢ (φ \land x = K) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x))$
88	80	fveq2d	$⊢ (φ \land x = K) \to C (⟨“ I J ”⟩) (x) = C (⟨“ I J ”⟩) (K)$
89	1 2 3 4 5 6 7 8 9	cyc2fvx	$⊢ φ \to C (⟨“ I J ”⟩) (K) = K$
90	89	adantr	$⊢ (φ \land x = K) \to C (⟨“ I J ”⟩) (K) = K$
91	88 90	eqtrd	$⊢ (φ \land x = K) \to C (⟨“ I J ”⟩) (x) = K$
92	91	fveq2d	$⊢ (φ \land x = K) \to C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x)) = C (⟨“ I K ”⟩) (K)$
93	1 3 4 6 18 2	cyc2fv2	$⊢ φ \to C (⟨“ I K ”⟩) (K) = I$
94	93	adantr	$⊢ (φ \land x = K) \to C (⟨“ I K ”⟩) (K) = I$
95	87 92 94	3eqtrd	$⊢ (φ \land x = K) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = I$
96	83 95	eqtrd	$⊢ (φ \land x = K) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = I$
97	79 81 96	3eqtr4d	$⊢ (φ \land x = K) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
98	97	adantlr	$⊢ ((φ \land x \in \{I, J, K\}) \land x = K) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
99		eltpi	$⊢ x \in \{I, J, K\} \to (x = I \lor x = J \lor x = K)$
100	99	adantl	$⊢ (φ \land x \in \{I, J, K\}) \to (x = I \lor x = J \lor x = K)$
101	56 77 98 100	mpjao3dan	$⊢ (φ \land x \in \{I, J, K\}) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
102	101	adantlr	$⊢ ((φ \land x \in D) \land x \in \{I, J, K\}) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
103	35	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I J ”⟩) : D ⟶ D$
104	103	ffund	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to Fun C (⟨“ I J ”⟩)$
105		simpr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to x \in (D ∖ \{I, J, K\})$
106	105	eldifad	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to x \in D$
107	39	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to dom C (⟨“ I J ”⟩) = D$
108	106 107	eleqtrrd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to x \in dom C (⟨“ I J ”⟩)$
109	104 108 42	syl2anc	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x))$
110	3	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to D \in V$
111	4 5	s2cld	$⊢ φ \to ⟨“ I J ”⟩ \in Word D$
112	111	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ⟨“ I J ”⟩ \in Word D$
113	4 5 7	s2f1	$⊢ φ \to ⟨“ I J ”⟩ : dom ⟨“ I J ”⟩ \underset{1-1}{⟶} D$
114	113	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ⟨“ I J ”⟩ : dom ⟨“ I J ”⟩ \underset{1-1}{⟶} D$
115		tpid1g	$⊢ I \in D \to I \in \{I, J, K\}$
116	4 115	syl	$⊢ φ \to I \in \{I, J, K\}$
117		tpid2g	$⊢ J \in D \to J \in \{I, J, K\}$
118	5 117	syl	$⊢ φ \to J \in \{I, J, K\}$
119	116 118	prssd	$⊢ φ \to \{I, J\} \subseteq \{I, J, K\}$
120	4 5	s2rn	$⊢ φ \to ran ⟨“ I J ”⟩ = \{I, J\}$
121	120	eqcomd	$⊢ φ \to \{I, J\} = ran ⟨“ I J ”⟩$
122	4 5 6	s3rn	$⊢ φ \to ran ⟨“ I J K ”⟩ = \{I, J, K\}$
123	122	eqcomd	$⊢ φ \to \{I, J, K\} = ran ⟨“ I J K ”⟩$
124	119 121 123	3sstr3d	$⊢ φ \to ran ⟨“ I J ”⟩ \subseteq ran ⟨“ I J K ”⟩$
125	124	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ran ⟨“ I J ”⟩ \subseteq ran ⟨“ I J K ”⟩$
126	105	eldifbd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \neg x \in \{I, J, K\}$
127	122	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ran ⟨“ I J K ”⟩ = \{I, J, K\}$
128	126 127	neleqtrrd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \neg x \in ran ⟨“ I J K ”⟩$
129	125 128	ssneldd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \neg x \in ran ⟨“ I J ”⟩$
130	1 110 112 114 106 129	cycpmfv3	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I J ”⟩) (x) = x$
131	130	fveq2d	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I K ”⟩) (C (⟨“ I J ”⟩) (x)) = C (⟨“ I K ”⟩) (x)$
132	4 6	s2cld	$⊢ φ \to ⟨“ I K ”⟩ \in Word D$
133	132	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ⟨“ I K ”⟩ \in Word D$
134	4 6 18	s2f1	$⊢ φ \to ⟨“ I K ”⟩ : dom ⟨“ I K ”⟩ \underset{1-1}{⟶} D$
135	134	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ⟨“ I K ”⟩ : dom ⟨“ I K ”⟩ \underset{1-1}{⟶} D$
136		tpid3g	$⊢ K \in D \to K \in \{I, J, K\}$
137	6 136	syl	$⊢ φ \to K \in \{I, J, K\}$
138	116 137	prssd	$⊢ φ \to \{I, K\} \subseteq \{I, J, K\}$
139	138	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \{I, K\} \subseteq \{I, J, K\}$
140	4 6	s2rn	$⊢ φ \to ran ⟨“ I K ”⟩ = \{I, K\}$
141	140	eqcomd	$⊢ φ \to \{I, K\} = ran ⟨“ I K ”⟩$
142	141	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \{I, K\} = ran ⟨“ I K ”⟩$
143	123	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \{I, J, K\} = ran ⟨“ I J K ”⟩$
144	139 142 143	3sstr3d	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ran ⟨“ I K ”⟩ \subseteq ran ⟨“ I J K ”⟩$
145	144 128	ssneldd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to \neg x \in ran ⟨“ I K ”⟩$
146	1 110 133 135 106 145	cycpmfv3	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I K ”⟩) (x) = x$
147	109 131 146	3eqtrd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x) = x$
148	31	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩) = C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)$
149	148	fveq1d	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x) = (C (⟨“ I K ”⟩) \circ C (⟨“ I J ”⟩)) (x)$
150	4 5 6	s3cld	$⊢ φ \to ⟨“ I J K ”⟩ \in Word D$
151	150	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ⟨“ I J K ”⟩ \in Word D$
152	4 5 6 7 8 9	s3f1	$⊢ φ \to ⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ \underset{1-1}{⟶} D$
153	152	adantr	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to ⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ \underset{1-1}{⟶} D$
154	1 110 151 153 106 128	cycpmfv3	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I J K ”⟩) (x) = x$
155	147 149 154	3eqtr4rd	$⊢ (φ \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
156	155	adantlr	$⊢ ((φ \land x \in D) \land x \in (D ∖ \{I, J, K\})) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
157		tpssi	$⊢ (I \in D \land J \in D \land K \in D) \to \{I, J, K\} \subseteq D$
158	4 5 6 157	syl3anc	$⊢ φ \to \{I, J, K\} \subseteq D$
159		undif	$⊢ \{I, J, K\} \subseteq D \leftrightarrow \{I, J, K\} \cup (D ∖ \{I, J, K\}) = D$
160	158 159	sylib	$⊢ φ \to \{I, J, K\} \cup (D ∖ \{I, J, K\}) = D$
161	160	eleq2d	$⊢ φ \to (x \in (\{I, J, K\} \cup (D ∖ \{I, J, K\})) \leftrightarrow x \in D)$
162	161	biimpar	$⊢ (φ \land x \in D) \to x \in (\{I, J, K\} \cup (D ∖ \{I, J, K\}))$
163		elun	$⊢ x \in (\{I, J, K\} \cup (D ∖ \{I, J, K\})) \leftrightarrow (x \in \{I, J, K\} \lor x \in (D ∖ \{I, J, K\}))$
164	162 163	sylib	$⊢ (φ \land x \in D) \to (x \in \{I, J, K\} \lor x \in (D ∖ \{I, J, K\}))$
165	102 156 164	mpjaodan	$⊢ (φ \land x \in D) \to C (⟨“ I J K ”⟩) (x) = (C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)) (x)$
166	15 25 165	eqfnfvd	$⊢ φ \to C (⟨“ I J K ”⟩) = C (⟨“ I K ”⟩) \underset{˙}{\cdot} C (⟨“ I J ”⟩)$

Metamath Proof Explorer

Theorem cyc3co2

Proof