Metamath Proof Explorer


Theorem gsumcom2

Description: Two-dimensional commutation of a group sum. Note that while A and D are constants w.r.t. j , k , C ( j ) and E ( k ) are not. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses gsum2d2.b 𝐵 = ( Base ‘ 𝐺 )
gsum2d2.z 0 = ( 0g𝐺 )
gsum2d2.g ( 𝜑𝐺 ∈ CMnd )
gsum2d2.a ( 𝜑𝐴𝑉 )
gsum2d2.r ( ( 𝜑𝑗𝐴 ) → 𝐶𝑊 )
gsum2d2.f ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐶 ) ) → 𝑋𝐵 )
gsum2d2.u ( 𝜑𝑈 ∈ Fin )
gsum2d2.n ( ( 𝜑 ∧ ( ( 𝑗𝐴𝑘𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
gsumcom2.d ( 𝜑𝐷𝑌 )
gsumcom2.c ( 𝜑 → ( ( 𝑗𝐴𝑘𝐶 ) ↔ ( 𝑘𝐷𝑗𝐸 ) ) )
Assertion gsumcom2 ( 𝜑 → ( 𝐺 Σg ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ) = ( 𝐺 Σg ( 𝑘𝐷 , 𝑗𝐸𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 gsum2d2.b 𝐵 = ( Base ‘ 𝐺 )
2 gsum2d2.z 0 = ( 0g𝐺 )
3 gsum2d2.g ( 𝜑𝐺 ∈ CMnd )
4 gsum2d2.a ( 𝜑𝐴𝑉 )
5 gsum2d2.r ( ( 𝜑𝑗𝐴 ) → 𝐶𝑊 )
6 gsum2d2.f ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐶 ) ) → 𝑋𝐵 )
7 gsum2d2.u ( 𝜑𝑈 ∈ Fin )
8 gsum2d2.n ( ( 𝜑 ∧ ( ( 𝑗𝐴𝑘𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
9 gsumcom2.d ( 𝜑𝐷𝑌 )
10 gsumcom2.c ( 𝜑 → ( ( 𝑗𝐴𝑘𝐶 ) ↔ ( 𝑘𝐷𝑗𝐸 ) ) )
11 snex { 𝑗 } ∈ V
12 xpexg ( ( { 𝑗 } ∈ V ∧ 𝐶𝑊 ) → ( { 𝑗 } × 𝐶 ) ∈ V )
13 11 5 12 sylancr ( ( 𝜑𝑗𝐴 ) → ( { 𝑗 } × 𝐶 ) ∈ V )
14 13 ralrimiva ( 𝜑 → ∀ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ∈ V )
15 iunexg ( ( 𝐴𝑉 ∧ ∀ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ∈ V ) → 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ∈ V )
16 4 14 15 syl2anc ( 𝜑 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ∈ V )
17 6 ralrimivva ( 𝜑 → ∀ 𝑗𝐴𝑘𝐶 𝑋𝐵 )
18 eqid ( 𝑗𝐴 , 𝑘𝐶𝑋 ) = ( 𝑗𝐴 , 𝑘𝐶𝑋 )
19 18 fmpox ( ∀ 𝑗𝐴𝑘𝐶 𝑋𝐵 ↔ ( 𝑗𝐴 , 𝑘𝐶𝑋 ) : 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ⟶ 𝐵 )
20 17 19 sylib ( 𝜑 → ( 𝑗𝐴 , 𝑘𝐶𝑋 ) : 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ⟶ 𝐵 )
21 1 2 3 4 5 6 7 8 gsum2d2lem ( 𝜑 → ( 𝑗𝐴 , 𝑘𝐶𝑋 ) finSupp 0 )
22 relxp Rel ( { 𝑘 } × 𝐸 )
23 22 rgenw 𝑘𝐷 Rel ( { 𝑘 } × 𝐸 )
24 reliun ( Rel 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↔ ∀ 𝑘𝐷 Rel ( { 𝑘 } × 𝐸 ) )
25 23 24 mpbir Rel 𝑘𝐷 ( { 𝑘 } × 𝐸 )
26 cnvf1o ( Rel 𝑘𝐷 ( { 𝑘 } × 𝐸 ) → ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto 𝑘𝐷 ( { 𝑘 } × 𝐸 ) )
27 25 26 ax-mp ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto 𝑘𝐷 ( { 𝑘 } × 𝐸 )
28 relxp Rel ( { 𝑗 } × 𝐶 )
29 28 rgenw 𝑗𝐴 Rel ( { 𝑗 } × 𝐶 )
30 reliun ( Rel 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ∀ 𝑗𝐴 Rel ( { 𝑗 } × 𝐶 ) )
31 29 30 mpbir Rel 𝑗𝐴 ( { 𝑗 } × 𝐶 )
32 relcnv Rel 𝑘𝐷 ( { 𝑘 } × 𝐸 )
33 nfv 𝑘 𝜑
34 nfv 𝑘𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 )
35 nfiu1 𝑘 𝑘𝐷 ( { 𝑘 } × 𝐸 )
36 35 nfcnv 𝑘 𝑘𝐷 ( { 𝑘 } × 𝐸 )
37 36 nfel2 𝑘𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 )
38 34 37 nfbi 𝑘 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) )
39 33 38 nfim 𝑘 ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
40 opeq2 ( 𝑘 = 𝑦 → ⟨ 𝑥 , 𝑘 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
41 40 eleq1d ( 𝑘 = 𝑦 → ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ) )
42 40 eleq1d ( 𝑘 = 𝑦 → ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
43 41 42 bibi12d ( 𝑘 = 𝑦 → ( ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ) )
44 43 imbi2d ( 𝑘 = 𝑦 → ( ( 𝜑 → ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ) ↔ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ) ) )
45 nfv 𝑗 𝜑
46 nfiu1 𝑗 𝑗𝐴 ( { 𝑗 } × 𝐶 )
47 46 nfel2 𝑗𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 )
48 nfv 𝑗𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 )
49 47 48 nfbi 𝑗 ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) )
50 45 49 nfim 𝑗 ( 𝜑 → ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
51 opeq1 ( 𝑗 = 𝑥 → ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑥 , 𝑘 ⟩ )
52 51 eleq1d ( 𝑗 = 𝑥 → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ) )
53 51 eleq1d ( 𝑗 = 𝑥 → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
54 52 53 bibi12d ( 𝑗 = 𝑥 → ( ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ↔ ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ) )
55 54 imbi2d ( 𝑗 = 𝑥 → ( ( 𝜑 → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ) ↔ ( 𝜑 → ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) ) ) )
56 opeliunxp ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑗𝐴𝑘𝐶 ) )
57 opeliunxp ( ⟨ 𝑘 , 𝑗 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↔ ( 𝑘𝐷𝑗𝐸 ) )
58 10 56 57 3bitr4g ( 𝜑 → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑘 , 𝑗 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
59 vex 𝑗 ∈ V
60 vex 𝑘 ∈ V
61 59 60 opelcnv ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↔ ⟨ 𝑘 , 𝑗 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) )
62 58 61 bitr4di ( 𝜑 → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
63 50 55 62 chvarfv ( 𝜑 → ( ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑘 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
64 39 44 63 chvarfv ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
65 31 32 64 eqrelrdv ( 𝜑 𝑗𝐴 ( { 𝑗 } × 𝐶 ) = 𝑘𝐷 ( { 𝑘 } × 𝐸 ) )
66 65 f1oeq3d ( 𝜑 → ( ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ) )
67 27 66 mpbiri ( 𝜑 → ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto 𝑗𝐴 ( { 𝑗 } × 𝐶 ) )
68 1 2 3 16 20 21 67 gsumf1o ( 𝜑 → ( 𝐺 Σg ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ) = ( 𝐺 Σg ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ∘ ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) ) ) )
69 sneq ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑧 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
70 69 cnveqd ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑧 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
71 70 unieqd ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑧 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
72 opswap { ⟨ 𝑥 , 𝑦 ⟩ } = ⟨ 𝑦 , 𝑥
73 71 72 eqtrdi ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑧 } = ⟨ 𝑦 , 𝑥 ⟩ )
74 73 fveq2d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) = ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ ⟨ 𝑦 , 𝑥 ⟩ ) )
75 df-ov ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) = ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ ⟨ 𝑦 , 𝑥 ⟩ )
76 74 75 eqtr4di ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) = ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) )
77 76 mpomptx ( 𝑧 𝑥𝐷 ( { 𝑥 } × 𝑥 / 𝑘 𝐸 ) ↦ ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) ) = ( 𝑥𝐷 , 𝑦 𝑥 / 𝑘 𝐸 ↦ ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) )
78 nfcv 𝑥 ( { 𝑘 } × 𝐸 )
79 nfcv 𝑘 { 𝑥 }
80 nfcsb1v 𝑘 𝑥 / 𝑘 𝐸
81 79 80 nfxp 𝑘 ( { 𝑥 } × 𝑥 / 𝑘 𝐸 )
82 sneq ( 𝑘 = 𝑥 → { 𝑘 } = { 𝑥 } )
83 csbeq1a ( 𝑘 = 𝑥𝐸 = 𝑥 / 𝑘 𝐸 )
84 82 83 xpeq12d ( 𝑘 = 𝑥 → ( { 𝑘 } × 𝐸 ) = ( { 𝑥 } × 𝑥 / 𝑘 𝐸 ) )
85 78 81 84 cbviun 𝑘𝐷 ( { 𝑘 } × 𝐸 ) = 𝑥𝐷 ( { 𝑥 } × 𝑥 / 𝑘 𝐸 )
86 85 mpteq1i ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) ) = ( 𝑧 𝑥𝐷 ( { 𝑥 } × 𝑥 / 𝑘 𝐸 ) ↦ ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) )
87 nfcv 𝑥 𝐸
88 nfcv 𝑥 ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 )
89 nfcv 𝑦 ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 )
90 nfcv 𝑘 𝑦
91 nfmpo2 𝑘 ( 𝑗𝐴 , 𝑘𝐶𝑋 )
92 nfcv 𝑘 𝑥
93 90 91 92 nfov 𝑘 ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 )
94 nfcv 𝑗 𝑦
95 nfmpo1 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 )
96 nfcv 𝑗 𝑥
97 94 95 96 nfov 𝑗 ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 )
98 oveq2 ( 𝑘 = 𝑥 → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) )
99 oveq1 ( 𝑗 = 𝑦 → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) = ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) )
100 98 99 sylan9eq ( ( 𝑘 = 𝑥𝑗 = 𝑦 ) → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) )
101 87 80 88 89 93 97 83 100 cbvmpox ( 𝑘𝐷 , 𝑗𝐸 ↦ ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) ) = ( 𝑥𝐷 , 𝑦 𝑥 / 𝑘 𝐸 ↦ ( 𝑦 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑥 ) )
102 77 86 101 3eqtr4i ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) ) = ( 𝑘𝐷 , 𝑗𝐸 ↦ ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) )
103 f1of ( ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto 𝑗𝐴 ( { 𝑗 } × 𝐶 ) → ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ⟶ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) )
104 67 103 syl ( 𝜑 → ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ⟶ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) )
105 eqid ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) = ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } )
106 105 fmpt ( ∀ 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) { 𝑧 } ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) : 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ⟶ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) )
107 104 106 sylibr ( 𝜑 → ∀ 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) { 𝑧 } ∈ 𝑗𝐴 ( { 𝑗 } × 𝐶 ) )
108 eqidd ( 𝜑 → ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) = ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) )
109 20 feqmptd ( 𝜑 → ( 𝑗𝐴 , 𝑘𝐶𝑋 ) = ( 𝑥 𝑗𝐴 ( { 𝑗 } × 𝐶 ) ↦ ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ 𝑥 ) ) )
110 fveq2 ( 𝑥 = { 𝑧 } → ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ 𝑥 ) = ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) )
111 107 108 109 110 fmptcof ( 𝜑 → ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ∘ ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) ) = ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ‘ { 𝑧 } ) ) )
112 6 ex ( 𝜑 → ( ( 𝑗𝐴𝑘𝐶 ) → 𝑋𝐵 ) )
113 18 ovmpt4g ( ( 𝑗𝐴𝑘𝐶𝑋𝐵 ) → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = 𝑋 )
114 113 3expia ( ( 𝑗𝐴𝑘𝐶 ) → ( 𝑋𝐵 → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = 𝑋 ) )
115 112 114 sylcom ( 𝜑 → ( ( 𝑗𝐴𝑘𝐶 ) → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = 𝑋 ) )
116 10 115 sylbird ( 𝜑 → ( ( 𝑘𝐷𝑗𝐸 ) → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = 𝑋 ) )
117 116 3impib ( ( 𝜑𝑘𝐷𝑗𝐸 ) → ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) = 𝑋 )
118 117 eqcomd ( ( 𝜑𝑘𝐷𝑗𝐸 ) → 𝑋 = ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) )
119 118 mpoeq3dva ( 𝜑 → ( 𝑘𝐷 , 𝑗𝐸𝑋 ) = ( 𝑘𝐷 , 𝑗𝐸 ↦ ( 𝑗 ( 𝑗𝐴 , 𝑘𝐶𝑋 ) 𝑘 ) ) )
120 102 111 119 3eqtr4a ( 𝜑 → ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ∘ ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) ) = ( 𝑘𝐷 , 𝑗𝐸𝑋 ) )
121 120 oveq2d ( 𝜑 → ( 𝐺 Σg ( ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ∘ ( 𝑧 𝑘𝐷 ( { 𝑘 } × 𝐸 ) ↦ { 𝑧 } ) ) ) = ( 𝐺 Σg ( 𝑘𝐷 , 𝑗𝐸𝑋 ) ) )
122 68 121 eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑗𝐴 , 𝑘𝐶𝑋 ) ) = ( 𝐺 Σg ( 𝑘𝐷 , 𝑗𝐸𝑋 ) ) )