Metamath Proof Explorer


Theorem dprd2d2

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dprd2d2.1 ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
dprd2d2.2 ( ( 𝜑𝑖𝐼 ) → 𝐺 dom DProd ( 𝑗𝐽𝑆 ) )
dprd2d2.3 ( 𝜑𝐺 dom DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) )
Assertion dprd2d2 ( 𝜑 → ( 𝐺 dom DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) ∧ ( 𝐺 DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) ) = ( 𝐺 DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dprd2d2.1 ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
2 dprd2d2.2 ( ( 𝜑𝑖𝐼 ) → 𝐺 dom DProd ( 𝑗𝐽𝑆 ) )
3 dprd2d2.3 ( 𝜑𝐺 dom DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) )
4 relxp Rel ( { 𝑖 } × 𝐽 )
5 4 rgenw 𝑖𝐼 Rel ( { 𝑖 } × 𝐽 )
6 reliun ( Rel 𝑖𝐼 ( { 𝑖 } × 𝐽 ) ↔ ∀ 𝑖𝐼 Rel ( { 𝑖 } × 𝐽 ) )
7 5 6 mpbir Rel 𝑖𝐼 ( { 𝑖 } × 𝐽 )
8 7 a1i ( 𝜑 → Rel 𝑖𝐼 ( { 𝑖 } × 𝐽 ) )
9 1 ralrimivva ( 𝜑 → ∀ 𝑖𝐼𝑗𝐽 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
10 eqid ( 𝑖𝐼 , 𝑗𝐽𝑆 ) = ( 𝑖𝐼 , 𝑗𝐽𝑆 )
11 10 fmpox ( ∀ 𝑖𝐼𝑗𝐽 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑖𝐼 , 𝑗𝐽𝑆 ) : 𝑖𝐼 ( { 𝑖 } × 𝐽 ) ⟶ ( SubGrp ‘ 𝐺 ) )
12 9 11 sylib ( 𝜑 → ( 𝑖𝐼 , 𝑗𝐽𝑆 ) : 𝑖𝐼 ( { 𝑖 } × 𝐽 ) ⟶ ( SubGrp ‘ 𝐺 ) )
13 dmiun dom 𝑖𝐼 ( { 𝑖 } × 𝐽 ) = 𝑖𝐼 dom ( { 𝑖 } × 𝐽 )
14 dmxpss dom ( { 𝑖 } × 𝐽 ) ⊆ { 𝑖 }
15 simpr ( ( 𝜑𝑖𝐼 ) → 𝑖𝐼 )
16 15 snssd ( ( 𝜑𝑖𝐼 ) → { 𝑖 } ⊆ 𝐼 )
17 14 16 sstrid ( ( 𝜑𝑖𝐼 ) → dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
18 17 ralrimiva ( 𝜑 → ∀ 𝑖𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
19 iunss ( 𝑖𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 ↔ ∀ 𝑖𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
20 18 19 sylibr ( 𝜑 𝑖𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
21 13 20 eqsstrid ( 𝜑 → dom 𝑖𝐼 ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
22 simprl ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑖𝐼 )
23 simprr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑗𝐽 )
24 10 ovmpt4g ( ( 𝑖𝐼𝑗𝐽𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) = 𝑆 )
25 22 23 1 24 syl3anc ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) = 𝑆 )
26 25 anassrs ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑗𝐽 ) → ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) = 𝑆 )
27 26 mpteq2dva ( ( 𝜑𝑖𝐼 ) → ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) = ( 𝑗𝐽𝑆 ) )
28 2 27 breqtrrd ( ( 𝜑𝑖𝐼 ) → 𝐺 dom DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) )
29 28 ralrimiva ( 𝜑 → ∀ 𝑖𝐼 𝐺 dom DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) )
30 nfcv 𝑖 𝐺
31 nfcv 𝑖 dom DProd
32 nfcsb1v 𝑖 𝑥 / 𝑖 𝐽
33 nfcv 𝑖 𝑥
34 nfmpo1 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 )
35 nfcv 𝑖 𝑗
36 33 34 35 nfov 𝑖 ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 )
37 32 36 nfmpt 𝑖 ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) )
38 30 31 37 nfbr 𝑖 𝐺 dom DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) )
39 csbeq1a ( 𝑖 = 𝑥𝐽 = 𝑥 / 𝑖 𝐽 )
40 oveq1 ( 𝑖 = 𝑥 → ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) = ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) )
41 39 40 mpteq12dv ( 𝑖 = 𝑥 → ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) = ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) )
42 41 breq2d ( 𝑖 = 𝑥 → ( 𝐺 dom DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ↔ 𝐺 dom DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) )
43 38 42 rspc ( 𝑥𝐼 → ( ∀ 𝑖𝐼 𝐺 dom DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) → 𝐺 dom DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) )
44 29 43 mpan9 ( ( 𝜑𝑥𝐼 ) → 𝐺 dom DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) )
45 nfcv 𝑦 ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 )
46 nfcv 𝑗 𝑥
47 nfmpo2 𝑗 ( 𝑖𝐼 , 𝑗𝐽𝑆 )
48 nfcv 𝑗 𝑦
49 46 47 48 nfov 𝑗 ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 )
50 oveq2 ( 𝑗 = 𝑦 → ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) = ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) )
51 45 49 50 cbvmpt ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) = ( 𝑦 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) )
52 nfv 𝑖 𝑗 = 𝑧
53 32 nfcri 𝑖 𝑗 𝑥 / 𝑖 𝐽
54 52 53 nfan 𝑖 ( 𝑗 = 𝑧𝑗 𝑥 / 𝑖 𝐽 )
55 39 eleq2d ( 𝑖 = 𝑥 → ( 𝑗𝐽𝑗 𝑥 / 𝑖 𝐽 ) )
56 55 anbi2d ( 𝑖 = 𝑥 → ( ( 𝑗 = 𝑧𝑗𝐽 ) ↔ ( 𝑗 = 𝑧𝑗 𝑥 / 𝑖 𝐽 ) ) )
57 54 56 equsexv ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧𝑗𝐽 ) ) ↔ ( 𝑗 = 𝑧𝑗 𝑥 / 𝑖 𝐽 ) )
58 simprl ( ( ( 𝜑𝑥𝐼 ) ∧ ( 𝑖 = 𝑥𝑗 = 𝑧 ) ) → 𝑖 = 𝑥 )
59 simplr ( ( ( 𝜑𝑥𝐼 ) ∧ ( 𝑖 = 𝑥𝑗 = 𝑧 ) ) → 𝑥𝐼 )
60 58 59 eqeltrd ( ( ( 𝜑𝑥𝐼 ) ∧ ( 𝑖 = 𝑥𝑗 = 𝑧 ) ) → 𝑖𝐼 )
61 60 biantrurd ( ( ( 𝜑𝑥𝐼 ) ∧ ( 𝑖 = 𝑥𝑗 = 𝑧 ) ) → ( 𝑗𝐽 ↔ ( 𝑖𝐼𝑗𝐽 ) ) )
62 61 pm5.32da ( ( 𝜑𝑥𝐼 ) → ( ( ( 𝑖 = 𝑥𝑗 = 𝑧 ) ∧ 𝑗𝐽 ) ↔ ( ( 𝑖 = 𝑥𝑗 = 𝑧 ) ∧ ( 𝑖𝐼𝑗𝐽 ) ) ) )
63 anass ( ( ( 𝑖 = 𝑥𝑗 = 𝑧 ) ∧ 𝑗𝐽 ) ↔ ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧𝑗𝐽 ) ) )
64 eqcom ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ↔ ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ )
65 vex 𝑖 ∈ V
66 vex 𝑗 ∈ V
67 65 66 opth ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ ↔ ( 𝑖 = 𝑥𝑗 = 𝑧 ) )
68 64 67 bitr2i ( ( 𝑖 = 𝑥𝑗 = 𝑧 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ )
69 68 anbi1i ( ( ( 𝑖 = 𝑥𝑗 = 𝑧 ) ∧ ( 𝑖𝐼𝑗𝐽 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) )
70 62 63 69 3bitr3g ( ( 𝜑𝑥𝐼 ) → ( ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧𝑗𝐽 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) ) )
71 70 exbidv ( ( 𝜑𝑥𝐼 ) → ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧𝑗𝐽 ) ) ↔ ∃ 𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) ) )
72 57 71 bitr3id ( ( 𝜑𝑥𝐼 ) → ( ( 𝑗 = 𝑧𝑗 𝑥 / 𝑖 𝐽 ) ↔ ∃ 𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) ) )
73 72 exbidv ( ( 𝜑𝑥𝐼 ) → ( ∃ 𝑗 ( 𝑗 = 𝑧𝑗 𝑥 / 𝑖 𝐽 ) ↔ ∃ 𝑗𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) ) )
74 vex 𝑧 ∈ V
75 eleq1w ( 𝑗 = 𝑧 → ( 𝑗 𝑥 / 𝑖 𝐽𝑧 𝑥 / 𝑖 𝐽 ) )
76 74 75 ceqsexv ( ∃ 𝑗 ( 𝑗 = 𝑧𝑗 𝑥 / 𝑖 𝐽 ) ↔ 𝑧 𝑥 / 𝑖 𝐽 )
77 excom ( ∃ 𝑗𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) ↔ ∃ 𝑖𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) )
78 73 76 77 3bitr3g ( ( 𝜑𝑥𝐼 ) → ( 𝑧 𝑥 / 𝑖 𝐽 ↔ ∃ 𝑖𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) ) )
79 elrelimasn ( Rel 𝑖𝐼 ( { 𝑖 } × 𝐽 ) → ( 𝑧 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↔ 𝑥 𝑖𝐼 ( { 𝑖 } × 𝐽 ) 𝑧 ) )
80 7 79 ax-mp ( 𝑧 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↔ 𝑥 𝑖𝐼 ( { 𝑖 } × 𝐽 ) 𝑧 )
81 df-br ( 𝑥 𝑖𝐼 ( { 𝑖 } × 𝐽 ) 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑖𝐼 ( { 𝑖 } × 𝐽 ) )
82 eliunxp ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑖𝐼 ( { 𝑖 } × 𝐽 ) ↔ ∃ 𝑖𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) )
83 80 81 82 3bitri ( 𝑧 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↔ ∃ 𝑖𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖𝐼𝑗𝐽 ) ) )
84 78 83 bitr4di ( ( 𝜑𝑥𝐼 ) → ( 𝑧 𝑥 / 𝑖 𝐽𝑧 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ) )
85 84 eqrdv ( ( 𝜑𝑥𝐼 ) → 𝑥 / 𝑖 𝐽 = ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) )
86 85 mpteq1d ( ( 𝜑𝑥𝐼 ) → ( 𝑦 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) = ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) )
87 51 86 syl5eq ( ( 𝜑𝑥𝐼 ) → ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) = ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) )
88 44 87 breqtrd ( ( 𝜑𝑥𝐼 ) → 𝐺 dom DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) )
89 27 oveq2d ( ( 𝜑𝑖𝐼 ) → ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) )
90 89 mpteq2dva ( 𝜑 → ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) ) = ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) )
91 3 90 breqtrrd ( 𝜑𝐺 dom DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) ) )
92 nfcv 𝑥 ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) )
93 nfcv 𝑖 DProd
94 30 93 37 nfov 𝑖 ( 𝐺 DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) )
95 41 oveq2d ( 𝑖 = 𝑥 → ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) )
96 92 94 95 cbvmpt ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) )
97 87 oveq2d ( ( 𝜑𝑥𝐼 ) → ( 𝐺 DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) )
98 97 mpteq2dva ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑗 𝑥 / 𝑖 𝐽 ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) ) )
99 96 98 syl5eq ( 𝜑 → ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽 ↦ ( 𝑖 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑗 ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) ) )
100 91 99 breqtrd ( 𝜑𝐺 dom DProd ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) ) )
101 eqid ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
102 8 12 21 88 100 101 dprd2da ( 𝜑𝐺 dom DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) )
103 8 12 21 88 100 101 dprd2db ( 𝜑 → ( 𝐺 DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) ) = ( 𝐺 DProd ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) ) ) )
104 99 90 eqtr3d ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) ) = ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) )
105 104 oveq2d ( 𝜑 → ( 𝐺 DProd ( 𝑥𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( 𝑖𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖𝐼 , 𝑗𝐽𝑆 ) 𝑦 ) ) ) ) ) = ( 𝐺 DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) ) )
106 103 105 eqtrd ( 𝜑 → ( 𝐺 DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) ) = ( 𝐺 DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) ) )
107 102 106 jca ( 𝜑 → ( 𝐺 dom DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) ∧ ( 𝐺 DProd ( 𝑖𝐼 , 𝑗𝐽𝑆 ) ) = ( 𝐺 DProd ( 𝑖𝐼 ↦ ( 𝐺 DProd ( 𝑗𝐽𝑆 ) ) ) ) ) )