Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐾 ”⟩ ) · ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) )