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 ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ 𝑋 ) ) )