Theorem 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	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
	cycpm3.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	cycpm3.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	cycpm3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	cycpm3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
	cycpm3.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
	cycpm3.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
	cycpm3.2	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
	cycpm3.3	⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
	cyc3co2.t	⊢ · = ( +g ‘ 𝑆 )
Assertion	cyc3co2	⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐾 ”⟩ ) · ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) )

Proof

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